Theorem reeanv 2944

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 1769	. 2 |- F/ y ph
2		nfv 1769	. 2 |- F/ x ps
3	1, 2	reean 2943	1 |- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )

Syntax hints:   <-> wb 189   /\ wa 376   E.wrex 2757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-ral 2761  df-rex 2762

This theorem is referenced by:  3reeanv  2945  2ralor  2946  disjxiun  4392  fliftfun  6223  tfrlem5  7116  uniinqs  7461  eroveu  7476  erovlem  7477  xpf1o  7752  unxpdomlem3  7796  unfi  7856  finsschain  7899  dffi3  7963  rankxplim3  8370  xpnum  8403  kmlem9  8606  sornom  8725  fpwwe2lem12  9084  cnegex  9832  zaddcl  11001  rexanre  13486  o1lo1  13678  o1co  13727  rlimcn2  13731  o1of2  13753  lo1add  13767  lo1mul  13768  summo  13860  ntrivcvgmul  14035  prodmolem2  14066  prodmo  14067  dvds2lem  14392  odd2np1  14443  bezoutlem4OLD  14585  bezoutlem4  14588  gcddiv  14596  opoe  14840  omoe  14841  opeo  14842  omeo  14843  pcqmul  14882  pcadd  14913  mul4sq  14977  4sqlem12  14979  prmgaplem7  15106  gaorber  17040  psgneu  17225  lsmsubm  17383  pj1eu  17424  efgredlem  17475  efgrelexlemb  17478  qusabl  17581  cygabl  17603  dprdsubg  17735  dvdsrtr  17958  unitgrp  17973  lss1d  18264  lsmspsn  18385  lspsolvlem  18443  lbsextlem2  18460  znfld  19208  cygznlem3  19217  psgnghm  19225  tgcl  20062  restbas  20251  ordtbas2  20284  uncmp  20495  txuni2  20657  txbas  20659  ptbasin  20669  txcnp  20712  txlly  20728  txnlly  20729  tx1stc  20742  tx2ndc  20743  fbasrn  20977  rnelfmlem  21045  fmfnfmlem3  21049  txflf  21099  qustgplem  21213  trust  21322  utoptop  21327  fmucndlem  21384  blin2  21522  metustto  21646  tgqioo  21896  minveclem3b  22448  minveclem3bOLD  22460  pmltpc  22479  evthicc2  22489  ovolunlem2  22529  dyaddisj  22633  rolle  23021  dvcvx  23051  itgsubst  23080  plyadd  23250  plymul  23251  coeeu  23258  aalioulem6  23372  dchrptlem2  24272  lgsdchr  24355  mul2sq  24372  2sqlem5  24375  pntibnd  24510  pntlemp  24527  cgraswap  24941  cgracom  24943  cgratr  24944  dfcgra2  24950  acopyeu  24954  ax5seg  25047  axpasch  25050  axeuclid  25072  axcontlem4  25076  axcontlem9  25081  usgra2edg  25188  frgrawopreglem5  25855  pjhthmo  27036  superpos  28088  chirredi  28128  cdjreui  28166  cdj3i  28175  xrofsup  28428  archiabllem2c  28586  ordtconlem1  28804  dya2iocnrect  29176  txpcon  30027  cvmlift2lem10  30107  cvmlift3lem7  30120  msubco  30241  mclsppslem  30293  ghomgrpilem2  30376  poseq  30562  soseq  30563  altopelaltxp  30814  funtransport  30869  btwnconn1lem13  30937  btwnconn1lem14  30938  segletr  30952  segleantisym  30953  funray  30978  funline  30980  tailfb  31104  mblfinlem3  32043  ismblfin  32045  itg2addnc  32060  ftc1anclem6  32086  heibor1lem  32205  crngohomfo  32303  ispridlc  32367  prter1  32515  hl2at  33041  cdlemn11pre  34849  dihord2pre  34864  dihord4  34897  dihmeetlem20N  34965  mapdpglem32  35344  diophin  35686  diophun  35687  iunrelexpuztr  36382  mullimc  37793  mullimcf  37800  addlimc  37826  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem80  38162  sge0resplit  38362  hoiqssbllem3  38564  2reu4a  38755  uhgr2edg  39453  2pthon3v-av  40065