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

Theorem eeanv 1854
Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
Assertion
Ref Expression
eeanv  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x ph  /\  E. y ps ) )
Distinct variable groups:    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem eeanv
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ y
ph
2 nfv 1605 . 2  |-  F/ x ps
31, 2eean 1853 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x ph  /\  E. y ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528
This theorem is referenced by:  eeeanv  1855  ee4anv  1856  pm11.07  2054  2eu4  2226  cgsex2g  2820  cgsex4g  2821  vtocl2  2839  spc2egv  2870  dtru  4201  copsex2t  4253  copsex2g  4254  xpnz  5099  fununi  5316  tfrlem7  6399  ener  6908  domtr  6914  unen  6943  undom  6950  sbthlem10  6980  mapen  7025  infxpenc2  7649  fseqen  7654  dfac5lem4  7753  zorn2lem6  8128  fpwwe2lem12  8263  genpnnp  8629  uzindOLD  10106  hashfacen  11392  summo  12190  iscatd2  13583  gictr  14739  gsumval3eu  15190  ptbasin  17272  txcls  17299  txbasval  17301  hmphtr  17474  reconn  18333  phtpcer  18493  pcohtpy  18518  mbfi1flimlem  19077  mbfmullem  19080  itg2add  19114  pconcon  23762  txscon  23772  wfrlem4  24259  wfrlem11  24266  frrlem4  24284  frrlem5c  24287  neibastop1  26308  riscer  26619  stoweidlem35  27784
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator