Theorem reeanv 3029

Description: Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
reeanv	|- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )

Distinct variable groups:   ph, y   ps, x   x, y   y, A   x, B

Allowed substitution hints:   ph( x)   ps( y)   A( x)   B( y)

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		nfv 1683	. 2 |- F/ y ph
2		nfv 1683	. 2 |- F/ x ps
3	1, 2	reean 3028	1 |- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )

Syntax hints:   <-> wb 184   /\ wa 369   E.wrex 2815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819  df-rex 2820

This theorem is referenced by:  3reeanv  3030  2ralor  3031  disjxiun  4444  fliftfun  6196  tfrlem5  7046  uniinqs  7388  eroveu  7403  erovlem  7404  xpf1o  7676  unxpdomlem3  7723  unfi  7783  finsschain  7823  dffi3  7887  rankxplim3  8295  xpnum  8328  kmlem9  8534  sornom  8653  fpwwe2lem12  9015  cnegex  9756  zaddcl  10899  rexanre  13138  o1lo1  13319  o1co  13368  rlimcn2  13372  o1of2  13394  lo1add  13408  lo1mul  13409  summo  13498  dvds2lem  13853  odd2np1  13901  bezoutlem4  14034  gcddiv  14042  opoe  14190  omoe  14191  opeo  14192  omeo  14193  pcqmul  14232  pcadd  14263  mul4sq  14327  4sqlem12  14329  gaorber  16141  psgneu  16327  lsmsubm  16469  pj1eu  16510  efgredlem  16561  efgrelexlemb  16564  divsabl  16664  cygabl  16684  dprdsubg  16861  dvdsrtr  17085  unitgrp  17100  lss1d  17392  lsmspsn  17513  lspsolvlem  17571  lbsextlem2  17588  znfld  18366  cygznlem3  18375  psgnghm  18383  tgcl  19237  restbas  19425  ordtbas2  19458  uncmp  19669  txuni2  19801  txbas  19803  ptbasin  19813  txcnp  19856  txlly  19872  txnlly  19873  tx1stc  19886  tx2ndc  19887  fbasrn  20120  rnelfmlem  20188  fmfnfmlem3  20192  txflf  20242  divstgplem  20354  trust  20467  utoptop  20472  fmucndlem  20529  blin2  20667  metusttoOLD  20795  metustto  20796  tgqioo  21040  minveclem3b  21578  pmltpc  21597  evthicc2  21607  ovolunlem2  21644  dyaddisj  21740  rolle  22126  dvcvx  22156  itgsubst  22185  plyadd  22349  plymul  22350  coeeu  22357  aalioulem6  22467  dchrptlem2  23268  lgsdchr  23351  mul2sq  23368  2sqlem5  23371  pntibnd  23506  pntlemp  23523  ax5seg  23917  axpasch  23920  axeuclid  23942  axcontlem4  23946  axcontlem9  23951  usgra2edg  24058  frgrawopreglem5  24725  pjhthmo  25896  superpos  26949  chirredi  26989  cdjreui  27027  cdj3i  27036  xrofsup  27250  archiabllem2c  27401  ordtconlem1  27542  dya2iocnrect  27892  txpcon  28317  cvmlift2lem10  28397  cvmlift3lem7  28410  ghomgrpilem2  28501  ntrivcvgmul  28613  prodmolem2  28644  prodmo  28645  poseq  28910  soseq  28911  altopelaltxp  29203  funtransport  29258  btwnconn1lem13  29326  btwnconn1lem14  29327  segletr  29341  segleantisym  29342  funray  29367  funline  29369  mblfinlem3  29630  ismblfin  29632  itg2addnc  29646  ftc1anclem6  29672  tailfb  29798  heibor1lem  29908  crngohomfo  30006  ispridlc  30070  prter1  30224  diophin  30310  diophun  30311  mullimc  31158  mullimcf  31165  addlimc  31190  fourierdlem42  31449  fourierdlem80  31487  2reu4a  31661  hl2at  34201  cdlemn11pre  36007  dihord2pre  36022  dihord4  36055  dihmeetlem20N  36123  mapdpglem32  36502