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

Theorem eeanv 1938
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 1630 . 2  |-  F/ y
ph
2 nfv 1630 . 2  |-  F/ x ps
31, 2eean 1937 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x ph  /\  E. y ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1551
This theorem is referenced by:  eeeanv  1939  eeeanvOLD  1940  ee4anv  1941  pm11.07OLD  2194  2eu4  2366  cgsex2g  2990  cgsex4g  2991  vtocl2  3009  spc2egv  3040  dtru  4392  copsex2t  4445  copsex2g  4446  xpnz  5294  fununi  5519  tfrlem7  6646  ener  7156  domtr  7162  unen  7191  undom  7198  sbthlem10  7228  mapen  7273  infxpenc2  7905  fseqen  7910  dfac5lem4  8009  zorn2lem6  8383  fpwwe2lem12  8518  genpnnp  8884  uzindOLD  10366  hashfacen  11705  summo  12513  iscatd2  13908  gictr  15064  gsumval3eu  15515  ptbasin  17611  txcls  17638  txbasval  17640  hmphtr  17817  reconn  18861  phtpcer  19022  pcohtpy  19047  mbfi1flimlem  19616  mbfmullem  19619  itg2add  19653  pconcon  24920  txscon  24930  ntrivcvgmul  25232  prodmo  25264  wfrlem4  25543  wfrlem11  25550  frrlem4  25587  frrlem5c  25590  neibastop1  26390  riscer  26606  fnchoice  27678  stoweidlem35  27762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator