Theorem reeanv 2835

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

Syntax hints:   <-> wb 177   /\ wa 359   E.wrex 2667

This theorem is referenced by:  3reeanv  2836  2ralor  2837  disjxiun  4169  fliftfun  5993  tfrlem5  6600  uniinqs  6943  eroveu  6958  erovlem  6959  xpf1o  7228  unxpdomlem3  7274  unfi  7333  finsschain  7371  dffi3  7394  rankxplim3  7761  xpnum  7794  kmlem9  7994  sornom  8113  fpwwe2lem12  8472  cnegex  9203  zaddcl  10273  rexanre  12105  o1lo1  12286  o1co  12335  rlimcn2  12339  o1of2  12361  lo1add  12375  lo1mul  12376  summo  12466  dvds2lem  12817  odd2np1  12863  bezoutlem4  12996  gcddiv  13004  opoe  13140  omoe  13141  opeo  13142  omeo  13143  pcqmul  13182  pcadd  13213  mul4sq  13277  4sqlem12  13279  gaorber  15040  lsmsubm  15242  pj1eu  15283  efgredlem  15334  efgrelexlemb  15337  divsabl  15435  cygabl  15455  dprdsubg  15537  dvdsrtr  15712  unitgrp  15727  lss1d  15994  lsmspsn  16111  lspsolvlem  16169  lbsextlem2  16186  znfld  16796  cygznlem3  16805  tgcl  16989  restbas  17176  ordtbas2  17209  uncmp  17420  txuni2  17550  txbas  17552  ptbasin  17562  txcnp  17605  txlly  17621  txnlly  17622  tx1stc  17635  tx2ndc  17636  fbasrn  17869  rnelfmlem  17937  fmfnfmlem3  17941  txflf  17991  divstgplem  18103  trust  18212  utoptop  18217  fmucndlem  18274  blin2  18412  metusttoOLD  18540  metustto  18541  tgqioo  18784  minveclem3b  19282  pmltpc  19300  evthicc2  19310  ovolunlem2  19347  dyaddisj  19441  rolle  19827  dvcvx  19857  itgsubst  19886  plyadd  20089  plymul  20090  coeeu  20097  aalioulem6  20207  dchrptlem2  21002  lgsdchr  21085  mul2sq  21102  2sqlem5  21105  pntibnd  21240  pntlemp  21257  usgra2edg  21355  pjhthmo  22757  superpos  23810  chirredi  23850  cdjreui  23888  cdj3i  23897  xrofsup  24079  dya2iocnrect  24584  txpcon  24872  cvmlift2lem10  24952  cvmlift3lem7  24965  ghomgrpilem2  25050  ntrivcvgmul  25183  prodmolem2  25214  prodmo  25215  poseq  25467  soseq  25468  altopelaltxp  25725  ax5seg  25781  axpasch  25784  axeuclid  25806  axcontlem4  25810  axcontlem9  25815  funtransport  25869  btwnconn1lem13  25937  btwnconn1lem14  25938  segletr  25952  segleantisym  25953  funray  25978  funline  25980  mblfinlem2  26144  ismblfin  26146  itg2addnc  26158  tailfb  26296  heibor1lem  26408  crngohomfo  26506  ispridlc  26570  prter1  26618  diophin  26721  diophun  26722  psgneu  27297  psgnghm  27305  2reu4a  27834  frgrawopreglem5  28151  hl2at  29887  cdlemn11pre  31693  dihord2pre  31708  dihord4  31741  dihmeetlem20N  31809  mapdpglem32  32188

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672