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

Theorem 19.41vv 1912
 Description: Version of 19.41 2101 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 1911 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑𝜓))
21exbii 1771 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑𝜓))
3 19.41v 1911 . 2 (∃𝑥(∃𝑦𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
42, 3bitri 264 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 384  ∃wex 1701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702 This theorem is referenced by:  19.41vvv  1913  rabxp  5119  copsex2gb  5196  mpt2mptx  6711  xpassen  8006  dfac5lem1  8898  fusgr2wsp2nb  27073  bnj996  30768  dfdm5  31413  dfrn5  31414  elima4  31416  brtxp2  31665  brpprod3a  31670  brimg  31721  brsuccf  31725  diblsmopel  35975  mpt2mptx2  41427
 Copyright terms: Public domain W3C validator