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

Theorem 19.41vv 1980
Description: Version of 19.41 2271 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)
Assertion
Ref Expression
19.41vv (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
Distinct variable groups:   𝜓,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem 19.41vv
StepHypRef Expression
1 19.41v 1979 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑𝜓))
21exbii 1878 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑𝜓))
3 19.41v 1979 . 2 (∃𝑥(∃𝑦𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
42, 3bitri 278 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 400  wex 1809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940
This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810
This theorem is referenced by:  19.41vvv  1981  cgsex4g  3501  rabxp  5711  copsex2gb  5795  mpomptx  7525  xpassen  9060  dfac5lem1  10108  fusgr2wsp2nb  30663  bnj996  35322  dfdm5  36243  dfrn5  36244  elima4  36246  brtxp2  36349  brpprod3a  36354  brimg  36405  lemsuccf  36409  brxrn2  39011  diblsmopel  41923  en2pr  44253  mpomptx2  49092
  Copyright terms: Public domain W3C validator