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

Theorem 19.42vv 2056
 Description: Version of 19.42 2280 with two quantifiers and a disjoint variable 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 2053 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.42v 2052 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
31, 2bitri 267 1 (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198   ∧ wa 386  ∃wex 1878 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009 This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879 This theorem is referenced by:  19.42vvv  2057  exdistr2  2058  3exdistr  2059  ceqsex3v  3463  ceqsex4v  3464  ceqsex8v  3466  elvvv  5415  xpdifid  5807  dfoprab2  6966  resoprab  7021  elrnmpt2res  7039  ov3  7062  ov6g  7063  oprabex3  7422  xpassen  8329  axaddf  10289  axmulf  10290  qqhval2  30567  bnj996  31567  cnfinltrel  33781  inxpxrn  34696  dvhopellsm  37187
 Copyright terms: Public domain W3C validator