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

Theorem 19.42vv 1907
 Description: Version of 19.42 2092 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 1906 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.42v 1905 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
31, 2bitri 263 1 (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696 This theorem is referenced by:  19.42vvv  1908  exdistr2  1909  3exdistr  1910  ceqsex3v  3219  ceqsex4v  3220  ceqsex8v  3222  elvvv  5101  xpdifid  5481  dfoprab2  6599  resoprab  6654  elrnmpt2res  6672  ov3  6695  ov6g  6696  oprabex3  7048  xpassen  7939  axaddf  9845  axmulf  9846  usgraedg4  25916  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  qqhval2  29354  bnj996  30279  dvhopellsm  35424
 Copyright terms: Public domain W3C validator