Theorem reeanv 3022

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 1712	. 2 |- F/ y ph
2		nfv 1712	. 2 |- F/ x ps
3	1, 2	reean 3021	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 367   E.wrex 2805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-ral 2809  df-rex 2810

This theorem is referenced by:  3reeanv  3023  2ralor  3024  disjxiun  4436  fliftfun  6185  tfrlem5  7041  uniinqs  7383  eroveu  7398  erovlem  7399  xpf1o  7672  unxpdomlem3  7719  unfi  7779  finsschain  7819  dffi3  7883  rankxplim3  8290  xpnum  8323  kmlem9  8529  sornom  8648  fpwwe2lem12  9008  cnegex  9750  zaddcl  10900  rexanre  13264  o1lo1  13445  o1co  13494  rlimcn2  13498  o1of2  13520  lo1add  13534  lo1mul  13535  summo  13624  ntrivcvgmul  13796  prodmolem2  13827  prodmo  13828  dvds2lem  14083  odd2np1  14133  bezoutlem4  14266  gcddiv  14274  opoe  14422  omoe  14423  opeo  14424  omeo  14425  pcqmul  14464  pcadd  14495  mul4sq  14559  4sqlem12  14561  gaorber  16548  psgneu  16733  lsmsubm  16875  pj1eu  16916  efgredlem  16967  efgrelexlemb  16970  qusabl  17073  cygabl  17095  dprdsubg  17269  dvdsrtr  17499  unitgrp  17514  lss1d  17807  lsmspsn  17928  lspsolvlem  17986  lbsextlem2  18003  znfld  18775  cygznlem3  18784  psgnghm  18792  tgcl  19641  restbas  19829  ordtbas2  19862  uncmp  20073  txuni2  20235  txbas  20237  ptbasin  20247  txcnp  20290  txlly  20306  txnlly  20307  tx1stc  20320  tx2ndc  20321  fbasrn  20554  rnelfmlem  20622  fmfnfmlem3  20626  txflf  20676  qustgplem  20788  trust  20901  utoptop  20906  fmucndlem  20963  blin2  21101  metusttoOLD  21229  metustto  21230  tgqioo  21474  minveclem3b  22012  pmltpc  22031  evthicc2  22041  ovolunlem2  22078  dyaddisj  22174  rolle  22560  dvcvx  22590  itgsubst  22619  plyadd  22783  plymul  22784  coeeu  22791  aalioulem6  22902  dchrptlem2  23741  lgsdchr  23824  mul2sq  23841  2sqlem5  23844  pntibnd  23979  pntlemp  23996  ax5seg  24446  axpasch  24449  axeuclid  24471  axcontlem4  24475  axcontlem9  24480  usgra2edg  24587  frgrawopreglem5  25253  pjhthmo  26421  superpos  27474  chirredi  27514  cdjreui  27552  cdj3i  27561  xrofsup  27819  archiabllem2c  27976  ordtconlem1  28144  dya2iocnrect  28492  txpcon  28944  cvmlift2lem10  29024  cvmlift3lem7  29037  msubco  29158  mclsppslem  29210  ghomgrpilem2  29293  poseq  29576  soseq  29577  altopelaltxp  29857  funtransport  29912  btwnconn1lem13  29980  btwnconn1lem14  29981  segletr  29995  segleantisym  29996  funray  30021  funline  30023  mblfinlem3  30296  ismblfin  30298  itg2addnc  30312  ftc1anclem6  30338  tailfb  30438  heibor1lem  30548  crngohomfo  30646  ispridlc  30710  prter1  30863  diophin  30948  diophun  30949  mullimc  31864  mullimcf  31871  addlimc  31896  fourierdlem42  32173  fourierdlem80  32211  2reu4a  32436  hl2at  35545  cdlemn11pre  37353  dihord2pre  37368  dihord4  37401  dihmeetlem20N  37469  mapdpglem32  37848  iunrelexpuztr  38227