Theorem cbvrexv 3085

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)

Hypothesis

Ref	Expression
cbvralv.1

Assertion

Ref	Expression
cbvrexv

Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		nfv 1707	. 2
3		cbvralv.1	. 2
4	1, 2, 3	cbvrex 3081	1

Syntax hints:  ->wi 4  <->wb 184  E.wrex 2808

This theorem is referenced by:  cbvrex2v  3093  reu7  3294  reusv3  4660  xpdifid  5440  fliftfun  6210  grpridd  6515  funcnvuni  6753  fun11iun  6760  nneob  7320  pssnn  7758  frfi  7785  finsschain  7847  marypha1lem  7913  supmo  7932  suplub2  7941  ordtypelem3  7966  ordtypelem9  7972  wemaplem1  7992  brwdom3  8029  unwdomg  8031  cantnf  8133  cantnfOLD  8155  trcl  8180  infxpenc2  8420  infxpenc2OLD  8424  aceq2  8521  dfac5lem4  8528  kmlem9  8559  kmlem14  8564  fin23lem26  8726  fin1a2lem13  8813  axdc3lem3  8853  winainflem  9092  axgroth4  9231  suprlub  10530  supmul1  10533  supmullem1  10534  supmullem2  10535  supmul  10536  ublbneg  11195  zsupss  11200  xrsupsslem  11527  xrinfmsslem  11528  fsuppmapnn0fiub  12097  rexanre  13179  rexuzre  13185  rexico  13186  caurcvg2  13500  caucvgb  13502  summolem2  13538  summo  13539  mertens  13695  prodmolem2  13742  prodmo  13743  odd2np1lem  14045  gcdcllem1  14149  pceu  14370  4sqlem12  14474  vdwlem10  14508  vdwlem13  14511  vdwnn  14516  drsdirfi  15567  gaorb  16345  psgnunilem3  16521  psgnunilem4  16522  psgneu  16531  pj1eu  16714  efgsfo  16757  cyggeninv  16886  cygabl  16893  pgpfac1lem5  17130  pgpfac1  17131  pgpfaclem2  17133  lss1d  17609  lspsneq  17768  lspsolvlem  17788  lbsextlem2  17805  mplcoe5lem  18130  cygznlem3  18608  pmatcollpw3fi1lem2  19288  ordtrest2lem  19704  cnprest  19790  1stcfb  19946  1stcelcls  19962  elpt  20073  fbssfi  20338  fgcl  20379  rnelfmlem  20453  fmfnfmlem3  20457  txflf  20507  alexsubb  20546  alexsubALTlem4  20550  isucn2  20782  icccmplem2  21328  ply1divex  22537  coeeu  22622  plydivex  22693  aannenlem2  22725  ulmcau  22790  ulmbdd  22793  dchrptlem2  23540  bposlem9  23567  pntibndlem3  23777  pntlemi  23789  pntlemp  23795  pntleml  23796  pnt3  23797  legval  23971  legov  23972  legov2  23973  lnopp2hpgb  24132  erclwwlksym  24814  erclwwlktr  24815  erclwwlknsym  24826  erclwwlkntr  24827  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  frgraregorufr0  25052  isgrpo2  25199  grpoidinvlem3  25208  isgrp2d  25237  isgrpda  25299  ubthlem3  25788  norm1exi  26168  pjhthmo  26220  cdjreui  27351  cdj3i  27360  isarchi3  27731  archiabl  27742  ordtrest2NEWlem  27904  lmxrge0  27934  esumcvg  28092  eulerpartlems  28299  eulerpartlemgvv  28315  conpcon  28680  cvmlift2lem12  28759  cvmlift2lem13  28760  cvmlift3lem2  28765  cvmlift3lem7  28770  cvmlift3  28773  poseq  29333  soseq  29334  funtransport  29681  funray  29790  funline  29792  supaddc  30041  supadd  30042  ptrest  30048  ismblfin  30055  volsupnfl  30059  itg2addnclem  30066  fnessref  30175  neibastop2  30179  unirep  30203  filbcmb  30231  sdclem1  30236  sdc  30237  fdc  30238  incsequz  30241  heibor1lem  30305  heiborlem10  30316  isdrngo2  30361  prnc  30464  prtlem13  30609  prtlem15  30616  mzpcompact2lem  30684  eldioph3  30699  diophrex  30709  rexrabdioph  30727  eldioph4i  30746  aomclem8  31007  hbtlem2  31073  rngunsnply  31122  dvconstbi  31239  expgrowth  31240  limcperiod  31634  limsupre  31647  cncfshiftioo  31695  itgiccshift  31779  itgperiod  31780  fourierdlem42  31931  fourierdlem48  31937  fourierdlem81  31970  fourierdlem92  31981  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem105  31994  fourierdlem108  31997  fourierdlem110  31999  fourierdlem112  32001  fourierdlem113  32002  2zlidl  32740  2zrngamgm  32745  2zrngagrp  32749  2zrngmmgm  32752  lshpsmreu  34834  lshpkrlem1  34835  lshpkrlem3  34837  pclfinN  35624  4atex  35800  dihglblem2N  37021  lcfl7N  37228  lcf1o  37278

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  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1613  df-nf 1617  df-sb 1740  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813