Theorem reeanv 2958

Description: Rearrange restricted 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 1761	. 2 |- F/ y ph
2		nfv 1761	. 2 |- F/ x ps
3	1, 2	reean 2957	1 |- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )

Syntax hints:   <-> wb 188   /\ wa 371   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-ral 2742  df-rex 2743

This theorem is referenced by:  3reeanv  2959  2ralor  2960  disjxiun  4399  fliftfun  6205  tfrlem5  7098  uniinqs  7443  eroveu  7458  erovlem  7459  xpf1o  7734  unxpdomlem3  7778  unfi  7838  finsschain  7881  dffi3  7945  rankxplim3  8352  xpnum  8385  kmlem9  8588  sornom  8707  fpwwe2lem12  9066  cnegex  9814  zaddcl  10977  rexanre  13409  o1lo1  13601  o1co  13650  rlimcn2  13654  o1of2  13676  lo1add  13690  lo1mul  13691  summo  13783  ntrivcvgmul  13958  prodmolem2  13989  prodmo  13990  dvds2lem  14315  odd2np1  14365  bezoutlem4OLD  14506  bezoutlem4  14509  gcddiv  14517  opoe  14761  omoe  14762  opeo  14763  omeo  14764  pcqmul  14803  pcadd  14834  mul4sq  14898  4sqlem12  14900  prmgaplem7  15027  gaorber  16962  psgneu  17147  lsmsubm  17305  pj1eu  17346  efgredlem  17397  efgrelexlemb  17400  qusabl  17503  cygabl  17525  dprdsubg  17657  dvdsrtr  17880  unitgrp  17895  lss1d  18186  lsmspsn  18307  lspsolvlem  18365  lbsextlem2  18382  znfld  19131  cygznlem3  19140  psgnghm  19148  tgcl  19985  restbas  20174  ordtbas2  20207  uncmp  20418  txuni2  20580  txbas  20582  ptbasin  20592  txcnp  20635  txlly  20651  txnlly  20652  tx1stc  20665  tx2ndc  20666  fbasrn  20899  rnelfmlem  20967  fmfnfmlem3  20971  txflf  21021  qustgplem  21135  trust  21244  utoptop  21249  fmucndlem  21306  blin2  21444  metustto  21568  tgqioo  21818  minveclem3b  22370  minveclem3bOLD  22382  pmltpc  22401  evthicc2  22411  ovolunlem2  22451  dyaddisj  22554  rolle  22942  dvcvx  22972  itgsubst  23001  plyadd  23171  plymul  23172  coeeu  23179  aalioulem6  23293  dchrptlem2  24193  lgsdchr  24276  mul2sq  24293  2sqlem5  24296  pntibnd  24431  pntlemp  24448  cgraswap  24862  cgracom  24864  cgratr  24865  dfcgra2  24871  acopyeu  24875  ax5seg  24968  axpasch  24971  axeuclid  24993  axcontlem4  24997  axcontlem9  25002  usgra2edg  25109  frgrawopreglem5  25776  pjhthmo  26955  superpos  28007  chirredi  28047  cdjreui  28085  cdj3i  28094  xrofsup  28353  archiabllem2c  28512  ordtconlem1  28730  dya2iocnrect  29103  txpcon  29955  cvmlift2lem10  30035  cvmlift3lem7  30048  msubco  30169  mclsppslem  30221  ghomgrpilem2  30304  poseq  30491  soseq  30492  altopelaltxp  30743  funtransport  30798  btwnconn1lem13  30866  btwnconn1lem14  30867  segletr  30881  segleantisym  30882  funray  30907  funline  30909  tailfb  31033  mblfinlem3  31979  ismblfin  31981  itg2addnc  31996  ftc1anclem6  32022  heibor1lem  32141  crngohomfo  32239  ispridlc  32303  prter1  32451  hl2at  32970  cdlemn11pre  34778  dihord2pre  34793  dihord4  34826  dihmeetlem20N  34894  mapdpglem32  35273  diophin  35615  diophun  35616  iunrelexpuztr  36311  mullimc  37696  mullimcf  37703  addlimc  37729  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem80  38050  sge0resplit  38248  hoiqssbllem3  38446  2reu4a  38610  usgr2edg  39291