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 1949
Description: Version of 19.41 2234 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 1948 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑𝜓))
21exbii 1847 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑𝜓))
3 19.41v 1948 . 2 (∃𝑥(∃𝑦𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
42, 3bitri 275 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779
This theorem is referenced by:  19.41vvv  1950  cgsex4g  3527  rabxp  5732  copsex2gb  5815  mpomptx  7547  xpassen  9107  dfac5lem1  10164  fusgr2wsp2nb  30354  bnj996  34971  dfdm5  35774  dfrn5  35775  elima4  35777  brtxp2  35883  brpprod3a  35888  brimg  35939  brsuccf  35943  brxrn2  38377  diblsmopel  41174  en2pr  43565  mpomptx2  48256
  Copyright terms: Public domain W3C validator