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

Theorem eeanv 1933
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 1626 . 2  |-  F/ y
ph
2 nfv 1626 . 2  |-  F/ x ps
31, 2eean 1932 1  |-  ( E. x E. y (
ph  /\  ps )  <->  ( E. x ph  /\  E. y ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547
This theorem is referenced by:  eeeanv  1934  eeeanvOLD  1935  ee4anv  1936  pm11.07OLD  2165  2eu4  2337  cgsex2g  2948  cgsex4g  2949  vtocl2  2967  spc2egv  2998  dtru  4350  copsex2t  4403  copsex2g  4404  xpnz  5251  fununi  5476  tfrlem7  6603  ener  7113  domtr  7119  unen  7148  undom  7155  sbthlem10  7185  mapen  7230  infxpenc2  7859  fseqen  7864  dfac5lem4  7963  zorn2lem6  8337  fpwwe2lem12  8472  genpnnp  8838  uzindOLD  10320  hashfacen  11658  summo  12466  iscatd2  13861  gictr  15017  gsumval3eu  15468  ptbasin  17562  txcls  17589  txbasval  17591  hmphtr  17768  reconn  18812  phtpcer  18973  pcohtpy  18998  mbfi1flimlem  19567  mbfmullem  19570  itg2add  19604  pconcon  24871  txscon  24881  ntrivcvgmul  25183  prodmo  25215  wfrlem4  25473  wfrlem11  25480  frrlem4  25498  frrlem5c  25501  neibastop1  26278  riscer  26494  fnchoice  27567  stoweidlem35  27651
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator