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 1951
Description: Version of 19.41 2237 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 1950 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑𝜓))
21exbii 1848 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑𝜓))
3 19.41v 1950 . 2 (∃𝑥(∃𝑦𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
42, 3bitri 277 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wex 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781
This theorem is referenced by:  19.41vvv  1952  rabxp  5574  copsex2gb  5653  mpomptx  7240  xpassen  8587  dfac5lem1  9525  fusgr2wsp2nb  28095  bnj996  32233  dfdm5  33021  dfrn5  33022  elima4  33024  brtxp2  33347  brpprod3a  33352  brimg  33403  brsuccf  33407  brxrn2  35660  diblsmopel  38340  en2pr  40028  mpomptx2  44513
  Copyright terms: Public domain W3C validator