Theorem reeanv 3025

Description: Rearrange restricted existential quantifiers. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
reeanv

Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		nfv 1707	. 2
3	1, 2	reean 3024	1

Syntax hints:  <->wb 184  /\wa 369  E.wrex 2808

This theorem is referenced by:  3reeanv  3026  2ralor  3027  disjxiun  4449  fliftfun  6210  tfrlem5  7068  uniinqs  7410  eroveu  7425  erovlem  7426  xpf1o  7699  unxpdomlem3  7746  unfi  7807  finsschain  7847  dffi3  7911  rankxplim3  8320  xpnum  8353  kmlem9  8559  sornom  8678  fpwwe2lem12  9040  cnegex  9782  zaddcl  10929  rexanre  13179  o1lo1  13360  o1co  13409  rlimcn2  13413  o1of2  13435  lo1add  13449  lo1mul  13450  summo  13539  ntrivcvgmul  13711  prodmolem2  13742  prodmo  13743  dvds2lem  13996  odd2np1  14046  bezoutlem4  14179  gcddiv  14187  opoe  14335  omoe  14336  opeo  14337  omeo  14338  pcqmul  14377  pcadd  14408  mul4sq  14472  4sqlem12  14474  gaorber  16346  psgneu  16531  lsmsubm  16673  pj1eu  16714  efgredlem  16765  efgrelexlemb  16768  qusabl  16871  cygabl  16893  dprdsubg  17071  dvdsrtr  17301  unitgrp  17316  lss1d  17609  lsmspsn  17730  lspsolvlem  17788  lbsextlem2  17805  znfld  18599  cygznlem3  18608  psgnghm  18616  tgcl  19471  restbas  19659  ordtbas2  19692  uncmp  19903  txuni2  20066  txbas  20068  ptbasin  20078  txcnp  20121  txlly  20137  txnlly  20138  tx1stc  20151  tx2ndc  20152  fbasrn  20385  rnelfmlem  20453  fmfnfmlem3  20457  txflf  20507  qustgplem  20619  trust  20732  utoptop  20737  fmucndlem  20794  blin2  20932  metusttoOLD  21060  metustto  21061  tgqioo  21305  minveclem3b  21843  pmltpc  21862  evthicc2  21872  ovolunlem2  21909  dyaddisj  22005  rolle  22391  dvcvx  22421  itgsubst  22450  plyadd  22614  plymul  22615  coeeu  22622  aalioulem6  22733  dchrptlem2  23540  lgsdchr  23623  mul2sq  23640  2sqlem5  23643  pntibnd  23778  pntlemp  23795  ax5seg  24241  axpasch  24244  axeuclid  24266  axcontlem4  24270  axcontlem9  24275  usgra2edg  24382  frgrawopreglem5  25048  pjhthmo  26220  superpos  27273  chirredi  27313  cdjreui  27351  cdj3i  27360  xrofsup  27582  archiabllem2c  27739  ordtconlem1  27906  dya2iocnrect  28252  txpcon  28677  cvmlift2lem10  28757  cvmlift3lem7  28770  msubco  28891  mclsppslem  28943  ghomgrpilem2  29026  poseq  29333  soseq  29334  altopelaltxp  29626  funtransport  29681  btwnconn1lem13  29749  btwnconn1lem14  29750  segletr  29764  segleantisym  29765  funray  29790  funline  29792  mblfinlem3  30053  ismblfin  30055  itg2addnc  30069  ftc1anclem6  30095  tailfb  30195  heibor1lem  30305  crngohomfo  30403  ispridlc  30467  prter1  30620  diophin  30706  diophun  30707  mullimc  31622  mullimcf  31629  addlimc  31654  fourierdlem42  31931  fourierdlem80  31969  2reu4a  32194  hl2at  35129  cdlemn11pre  36937  dihord2pre  36952  dihord4  36985  dihmeetlem20N  37053  mapdpglem32  37432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-ral 2812  df-rex 2813