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

Theorem eeanv 2170
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 1830 . 2 𝑦𝜑
2 nfv 1830 . 2 𝑥𝜓
31, 2eean 2169 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701
This theorem is referenced by:  eeeanv  2171  ee4anv  2172  2mo2  2538  cgsex2g  3212  cgsex4g  3213  vtocl2  3234  spc2egv  3268  dtru  4783  copsex2t  4883  copsex2g  4884  xpnz  5472  fununi  5878  wfrlem4  7305  wfrfun  7312  tfrlem7  7366  ener  7888  enerOLD  7889  domtr  7895  unen  7925  undom  7933  sbthlem10  7964  mapen  8009  infxpenc2  8728  fseqen  8733  dfac5lem4  8832  zorn2lem6  9206  fpwwe2lem12  9342  genpnnp  9706  hashfacen  13095  summo  14295  ntrivcvgmul  14473  prodmo  14505  iscatd2  16165  gictr  17540  gsumval3eu  18128  ptbasin  21190  txcls  21217  txbasval  21219  hmphtr  21396  reconn  22439  phtpcer  22602  phtpcerOLD  22603  pcohtpy  22628  mbfi1flimlem  23295  mbfmullem  23298  itg2add  23332  spc2ed  28696  brabgaf  28800  pconcon  30467  txscon  30477  frrlem4  31027  frrlem5c  31030  neibastop1  31524  bj-dtru  31985  riscer  32957  fnchoice  38211  fzisoeu  38455  stoweidlem35  38928
  Copyright terms: Public domain W3C validator