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

Theorem eeanv 2169
Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
Assertion
Ref Expression
eeanv (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem eeanv
StepHypRef Expression
1 nfv 1829 . 2 𝑦𝜑
2 nfv 1829 . 2 𝑥𝜓
31, 2eean 2168 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1700
This theorem is referenced by:  eeeanv  2170  ee4anv  2171  2mo2  2537  cgsex2g  3211  cgsex4g  3212  vtocl2  3233  spc2egv  3267  dtru  4778  copsex2t  4877  copsex2g  4878  xpnz  5458  fununi  5864  wfrlem4  7282  wfrfun  7289  tfrlem7  7343  ener  7865  enerOLD  7866  domtr  7872  unen  7902  undom  7910  sbthlem10  7941  mapen  7986  infxpenc2  8705  fseqen  8710  dfac5lem4  8809  zorn2lem6  9183  fpwwe2lem12  9319  genpnnp  9683  hashfacen  13047  summo  14241  ntrivcvgmul  14419  prodmo  14451  iscatd2  16111  gictr  17486  gsumval3eu  18074  ptbasin  21132  txcls  21159  txbasval  21161  hmphtr  21338  reconn  22371  phtpcer  22533  phtpcerOLD  22534  pcohtpy  22559  mbfi1flimlem  23212  mbfmullem  23215  itg2add  23249  spc2ed  28502  brabgaf  28606  pconcon  30273  txscon  30283  frrlem4  30833  frrlem5c  30836  neibastop1  31330  bj-dtru  31791  riscer  32753  fnchoice  38007  fzisoeu  38251  stoweidlem35  38725
  Copyright terms: Public domain W3C validator