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