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 1953
Description: Version of 19.42 2224 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 1950 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.42v 1949 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
31, 2bitri 274 1 (∃𝑥𝑦(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774
This theorem is referenced by:  exdistr2  1954  3exdistr  1956  cgsex4g  3509  ceqsex3v  3521  ceqsex4v  3522  ceqsex8v  3524  elvvv  5753  xpdifid  6174  dfoprab2  7478  resoprab  7538  elrnmpores  7559  ov3  7584  ov6g  7585  oprabex3  7982  xpassen  9094  entrfil  9216  domtrfil  9223  sbthfilem  9229  axaddf  11175  axmulf  11176  catcone0  17686  qqhval2  33734  bnj996  34738  fineqvac  34868  inxpxrn  38017  dvhopellsm  40740
  Copyright terms: Public domain W3C validator