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 1917
Description: Version of 19.42 2103 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 1916 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.42v 1915 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
31, 2bitri 264 1 (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702
This theorem is referenced by:  19.42vvv  1918  exdistr2  1919  3exdistr  1920  ceqsex3v  3232  ceqsex4v  3233  ceqsex8v  3235  elvvv  5139  xpdifid  5521  dfoprab2  6654  resoprab  6709  elrnmpt2res  6727  ov3  6750  ov6g  6751  oprabex3  7102  xpassen  7998  axaddf  9910  axmulf  9911  qqhval2  29808  bnj996  30733  dvhopellsm  35886
  Copyright terms: Public domain W3C validator