Theorem reeanv 2878

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 1672	. 2 |- F/ y ph
2		nfv 1672	. 2 |- F/ x ps
3	1, 2	reean 2877	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 2706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711

This theorem is referenced by:  3reeanv  2879  2ralor  2880  disjxiun  4277  fliftfun  5992  tfrlem5  6825  uniinqs  7168  eroveu  7183  erovlem  7184  xpf1o  7461  unxpdomlem3  7507  unfi  7567  finsschain  7606  dffi3  7669  rankxplim3  8076  xpnum  8109  kmlem9  8315  sornom  8434  fpwwe2lem12  8795  cnegex  9537  zaddcl  10672  rexanre  12817  o1lo1  12998  o1co  13047  rlimcn2  13051  o1of2  13073  lo1add  13087  lo1mul  13088  summo  13177  dvds2lem  13527  odd2np1  13574  bezoutlem4  13707  gcddiv  13715  opoe  13860  omoe  13861  opeo  13862  omeo  13863  pcqmul  13902  pcadd  13933  mul4sq  13997  4sqlem12  13999  gaorber  15805  psgneu  15991  lsmsubm  16131  pj1eu  16172  efgredlem  16223  efgrelexlemb  16226  divsabl  16326  cygabl  16346  dprdsubg  16494  dvdsrtr  16677  unitgrp  16692  lss1d  16965  lsmspsn  17086  lspsolvlem  17144  lbsextlem2  17161  znfld  17834  cygznlem3  17843  psgnghm  17851  tgcl  18415  restbas  18603  ordtbas2  18636  uncmp  18847  txuni2  18979  txbas  18981  ptbasin  18991  txcnp  19034  txlly  19050  txnlly  19051  tx1stc  19064  tx2ndc  19065  fbasrn  19298  rnelfmlem  19366  fmfnfmlem3  19370  txflf  19420  divstgplem  19532  trust  19645  utoptop  19650  fmucndlem  19707  blin2  19845  metusttoOLD  19973  metustto  19974  tgqioo  20218  minveclem3b  20756  pmltpc  20775  evthicc2  20785  ovolunlem2  20822  dyaddisj  20917  rolle  21303  dvcvx  21333  itgsubst  21362  plyadd  21569  plymul  21570  coeeu  21577  aalioulem6  21687  dchrptlem2  22488  lgsdchr  22571  mul2sq  22588  2sqlem5  22591  pntibnd  22726  pntlemp  22743  ax5seg  23006  axpasch  23009  axeuclid  23031  axcontlem4  23035  axcontlem9  23040  usgra2edg  23123  pjhthmo  24527  superpos  25580  chirredi  25620  cdjreui  25658  cdj3i  25667  xrofsup  25877  archiabllem2c  26035  ordtconlem1  26207  dya2iocnrect  26549  txpcon  26968  cvmlift2lem10  27048  cvmlift3lem7  27061  ghomgrpilem2  27151  ntrivcvgmul  27263  prodmolem2  27294  prodmo  27295  poseq  27560  soseq  27561  altopelaltxp  27853  funtransport  27908  btwnconn1lem13  27976  btwnconn1lem14  27977  segletr  27991  segleantisym  27992  funray  28017  funline  28019  mblfinlem3  28271  ismblfin  28273  itg2addnc  28287  ftc1anclem6  28313  tailfb  28439  heibor1lem  28549  crngohomfo  28647  ispridlc  28711  prter1  28866  diophin  28953  diophun  28954  2reu4a  29856  frgrawopreglem5  30484  hl2at  32619  cdlemn11pre  34425  dihord2pre  34440  dihord4  34473  dihmeetlem20N  34541  mapdpglem32  34920