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 1957
Description: Version of 19.42 2236 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 1954 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.42v 1953 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
31, 2bitri 275 1 (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780
This theorem is referenced by:  exdistr2  1958  3exdistr  1960  cgsex4g  3528  ceqsex3v  3537  ceqsex4v  3538  ceqsex8v  3540  elvvv  5761  xpdifid  6188  dfoprab2  7491  resoprab  7551  elrnmpores  7571  ov3  7596  ov6g  7597  oprabex3  8002  xpassen  9106  entrfil  9225  domtrfil  9232  sbthfilem  9238  axaddf  11185  axmulf  11186  catcone0  17730  qqhval2  33983  bnj996  34970  fineqvac  35111  inxpxrn  38396  dvhopellsm  41119
  Copyright terms: Public domain W3C validator