MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.42vv Structured version   Visualization version   GIF version

Theorem 19.42vv 1923
Description: Version of 19.42 2143 with two quantifiers and a dv condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.)
Assertion
Ref Expression
19.42vv (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem 19.42vv
StepHypRef Expression
1 exdistr 1922 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.42v 1921 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
31, 2bitri 264 1 (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745
This theorem is referenced by:  19.42vvv  1924  exdistr2  1925  3exdistr  1926  ceqsex3v  3277  ceqsex4v  3278  ceqsex8v  3280  elvvv  5212  xpdifid  5597  dfoprab2  6743  resoprab  6798  elrnmpt2res  6816  ov3  6839  ov6g  6840  oprabex3  7199  xpassen  8095  axaddf  10004  axmulf  10005  qqhval2  30154  bnj996  31151  inxpxrn  34293  dvhopellsm  36723
  Copyright terms: Public domain W3C validator