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 2049
Description: Version of 19.41 2278 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 2048 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑𝜓))
21exbii 1947 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑𝜓))
3 19.41v 2048 . 2 (∃𝑥(∃𝑦𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
42, 3bitri 267 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  wex 1878
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879
This theorem is referenced by:  19.41vvv  2050  rabxp  5391  copsex2gb  5468  mpt2mptx  7016  xpassen  8329  dfac5lem1  9266  fusgr2wsp2nb  27711  bnj996  31567  dfdm5  32209  dfrn5  32210  elima4  32212  brtxp2  32522  brpprod3a  32527  brimg  32578  brsuccf  32582  brxrn2  34680  diblsmopel  37241  mpt2mptx2  42974
  Copyright terms: Public domain W3C validator