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

Theorem eeanv 2344
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 1995 . 2 𝑦𝜑
2 nfv 1995 . 2 𝑥𝜓
31, 2eean 2343 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-ex 1853  df-nf 1858
This theorem is referenced by:  eeeanv  2345  ee4anv  2346  2mo2  2699  cgsex2g  3391  cgsex4g  3392  vtocl2  3412  spc2egv  3446  dtru  4988  copsex2t  5084  copsex2g  5085  xpnz  5694  fununi  6104  wfrlem4  7570  wfrlem4OLD  7571  wfrfun  7578  tfrlem7  7632  ener  8156  domtr  8162  unen  8196  undom  8204  sbthlem10  8235  mapen  8280  infxpenc2  9045  fseqen  9050  dfac5lem4  9149  zorn2lem6  9525  fpwwe2lem12  9665  genpnnp  10029  hashfacen  13440  summo  14656  ntrivcvgmul  14841  prodmo  14873  iscatd2  16549  gictr  17925  gsumval3eu  18512  ptbasin  21601  txcls  21628  txbasval  21630  hmphtr  21807  reconn  22851  phtpcer  23014  pcohtpy  23039  mbfi1flimlem  23709  mbfmullem  23712  itg2add  23746  spc2ed  29652  brabgaf  29758  pconnconn  31551  txsconn  31561  frrlem4  32120  frrlem5c  32123  neibastop1  32691  bj-dtru  33133  riscer  34119  br1cosscnvxrn  34566  fnchoice  39710  fzisoeu  40031  stoweidlem35  40769  elsprel  42253
  Copyright terms: Public domain W3C validator