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 1918
Description: Version of 19.41 2141 with two quantifiers and a dv 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 1917 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑𝜓))
21exbii 1814 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑𝜓))
3 19.41v 1917 . 2 (∃𝑥(∃𝑦𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
42, 3bitri 264 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745
This theorem is referenced by:  19.41vvv  1919  rabxp  5188  copsex2gb  5263  mpt2mptx  6793  xpassen  8095  dfac5lem1  8984  fusgr2wsp2nb  27314  bnj996  31151  dfdm5  31800  dfrn5  31801  elima4  31803  brtxp2  32113  brpprod3a  32118  brimg  32169  brsuccf  32173  brxrn2  34277  diblsmopel  36777  mpt2mptx2  42438
  Copyright terms: Public domain W3C validator