Theorem eeanv 1988

Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)

Assertion

Ref	Expression
eeanv

Distinct variable groups:   ,   ,

Proof of Theorem eeanv

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		nfv 1707	. 2
3	1, 2	eean 1987	1

Syntax hints:  <->wb 184  /\wa 369  E.wex 1612

This theorem is referenced by:  eeeanv  1989  ee4anv  1990  2mo2  2372  2eu4OLD  2381  cgsex2g  3143  cgsex4g  3144  vtocl2  3162  spc2egv  3196  dtru  4643  copsex2t  4739  copsex2g  4740  xpnz  5431  fununi  5659  tfrlem7  7071  ener  7582  domtr  7588  unen  7618  undom  7625  sbthlem10  7656  mapen  7701  infxpenc2  8420  infxpenc2OLD  8424  fseqen  8429  dfac5lem4  8528  zorn2lem6  8902  fpwwe2lem12  9040  genpnnp  9404  uzindOLD  10982  hashfacen  12503  summo  13539  ntrivcvgmul  13711  prodmo  13743  iscatd2  15078  gictr  16323  gsumval3eu  16907  ptbasin  20078  txcls  20105  txbasval  20107  hmphtr  20284  reconn  21333  phtpcer  21495  pcohtpy  21520  mbfi1flimlem  22129  mbfmullem  22132  itg2add  22166  spc2ed  27372  pconcon  28676  txscon  28686  wfrlem4  29346  wfrlem11  29353  frrlem4  29390  frrlem5c  29393  neibastop1  30177  riscer  30391  fnchoice  31404  fzisoeu  31500  stoweidlem35  31817  bj-dtru  34383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617