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

Theorem eeanv 1918
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 1619 . 2  |-  F/ y
ph
2 nfv 1619 . 2  |-  F/ x ps
31, 2eean 1917 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 1541
This theorem is referenced by:  eeeanv  1919  ee4anv  1920  pm11.07  2120  2eu4  2292  cgsex2g  2896  cgsex4g  2897  vtocl2  2915  spc2egv  2946  dtru  4282  copsex2t  4335  copsex2g  4336  xpnz  5181  fununi  5398  tfrlem7  6486  ener  6996  domtr  7002  unen  7031  undom  7038  sbthlem10  7068  mapen  7113  infxpenc2  7739  fseqen  7744  dfac5lem4  7843  zorn2lem6  8218  fpwwe2lem12  8353  genpnnp  8719  uzindOLD  10198  hashfacen  11488  summo  12287  iscatd2  13682  gictr  14838  gsumval3eu  15289  ptbasin  17378  txcls  17405  txbasval  17407  hmphtr  17580  reconn  18436  phtpcer  18597  pcohtpy  18622  mbfi1flimlem  19181  mbfmullem  19184  itg2add  19218  pconcon  24166  txscon  24176  ntrivcvgmul  24531  prodmo  24563  wfrlem4  24817  wfrlem11  24824  frrlem4  24842  frrlem5c  24845  neibastop1  25632  riscer  25942  stoweidlem35  27107
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545
  Copyright terms: Public domain W3C validator