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 1947
Description: Version of 19.41 2224 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 1946 . . 3 (∃𝑦(𝜑𝜓) ↔ (∃𝑦𝜑𝜓))
21exbii 1843 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(∃𝑦𝜑𝜓))
3 19.41v 1946 . 2 (∃𝑥(∃𝑦𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
42, 3bitri 274 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝑦𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775
This theorem is referenced by:  19.41vvv  1948  cgsex4g  3513  rabxp  5722  copsex2gb  5804  mpomptx  7529  xpassen  9095  dfac5lem1  10158  fusgr2wsp2nb  30263  bnj996  34813  dfdm5  35608  dfrn5  35609  elima4  35611  brtxp2  35717  brpprod3a  35722  brimg  35773  brsuccf  35777  brxrn2  38085  diblsmopel  40882  en2pr  43250  mpomptx2  47748
  Copyright terms: Public domain W3C validator