Theorem cbvrexv 3401

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:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrexv

Step	Hyp	Ref	Expression
1		nfv 1890	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1890	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvralv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvrex 3397	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 207  ∃wrex 3104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109

This theorem is referenced by:  cbvrex2v  3410  reu7  3652  disjiund  4947  reusv3  5190  xpdifid  5893  fliftfun  6919  grpridd  7235  funcnvuni  7483  fiunlem  7490  nneob  8120  pssnn  8572  frfi  8599  finsschain  8667  marypha1lem  8733  supmo  8752  suplub2  8761  infmo  8795  ordtypelem3  8820  ordtypelem9  8826  wemaplem1  8846  brwdom3  8882  unwdomg  8884  cantnf  8991  trcl  9005  infxpenc2  9283  aceq2  9380  dfac5lem4  9387  kmlem9  9419  kmlem14  9424  fin23lem26  9582  fin1a2lem13  9669  axdc3lem3  9709  winainflem  9950  axgroth4  10089  suprlub  11442  supaddc  11445  supadd  11446  supmul1  11447  supmullem1  11448  supmullem2  11449  supmul  11450  ublbneg  12171  zsupss  12175  xrsupsslem  12539  xrinfmsslem  12540  rexanre  14528  rexuzre  14534  rexico  14535  caurcvg2  14856  caucvgb  14858  summolem2  14894  summo  14895  mertens  15063  prodmolem2  15110  prodmo  15111  odd2np1lem  15510  gcdcllem1  15669  pceu  16000  4sqlem12  16109  vdwlem10  16143  vdwlem13  16146  vdwnn  16151  drsdirfi  17365  dfgrp2  17874  dfgrp3lem  17942  gaorb  18166  psgnunilem3  18343  psgnunilem4  18344  psgneu  18353  pj1eu  18537  efgsfo  18580  cyggeninv  18713  cygabl  18720  pgpfac1lem5  18906  pgpfac1  18907  pgpfaclem2  18909  lss1d  19413  lspsneq  19572  lspsolvlem  19592  lbsextlem2  19609  mplcoe5lem  19923  cygznlem3  20386  pmatcollpw3fi1lem2  21067  ordtrest2lem  21483  cnprest  21569  1stcfb  21725  1stcelcls  21741  elpt  21852  fbssfi  22117  fgcl  22158  rnelfmlem  22232  fmfnfmlem3  22236  txflf  22286  alexsubb  22326  alexsubALTlem4  22330  isucn2  22559  icccmplem2  23102  ply1divex  24401  coeeu  24486  plydivex  24557  aannenlem2  24589  ulmcau  24654  ulmbdd  24657  dchrptlem2  25511  bposlem9  25538  2lgslem1b  25638  pntibndlem3  25838  pntlemi  25850  pntlemp  25856  pntleml  25857  pnt3  25858  legval  26040  legov  26041  legov2  26042  outpasch  26211  lnopp2hpgb  26219  colopp  26225  erclwwlksym  27474  erclwwlktr  27475  erclwwlknsym  27524  erclwwlkntr  27525  eleclclwwlkn  27530  hashecclwwlkn1  27531  umgrhashecclwwlk  27532  grpoidinvlem3  27962  ubthlem3  28328  norm1exi  28706  pjhthmo  28758  cdjreui  29888  cdj3i  29897  infxrge0glb  30150  cyc3genpm  30390  isarchi3  30412  archiabl  30423  ordtrest2NEWlem  30738  lmxrge0  30768  esumcvg  30918  esum2d  30925  eulerpartlems  31191  eulerpartlemgvv  31207  connpconn  32046  cvmlift2lem12  32125  cvmlift2lem13  32126  cvmlift3lem2  32131  cvmlift3lem7  32136  cvmlift3  32139  fmlasuc  32195  fmla1  32196  satffunlem1lem1  32210  satffunlem2lem1  32212  poseq  32649  soseq  32650  noprefixmo  32756  nosupdm  32758  nosupfv  32760  nosupres  32761  nosupbnd1lem1  32762  nosupbnd1lem4  32765  funtransport  33046  funray  33155  funline  33157  fnessref  33259  neibastop2  33263  dissneqlem  34098  dissneq  34099  pibt2  34175  ptrest  34368  poimirlem27  34396  poimirlem32  34401  ismblfin  34410  volsupnfl  34414  itg2addnclem  34420  unirep  34466  filbcmb  34493  sdclem1  34496  sdc  34497  fdc  34498  incsequz  34501  heibor1lem  34565  heiborlem10  34576  isgrpda  34711  isdrngo2  34714  prnc  34823  prtlem13  35485  prtlem15  35492  lshpsmreu  35726  lshpkrlem1  35727  lshpkrlem3  35729  pclfinN  36517  4atex  36693  dihglblem2N  37911  lcfl7N  38118  lcf1o  38168  mzpcompact2lem  38783  eldioph3  38798  diophrex  38808  rexrabdioph  38827  eldioph4i  38845  aomclem8  39097  hbtlem2  39160  rngunsnply  39209  iunrelexpuztr  39500  ntrclsneine0lem  39850  rexlimdvaacbv  39998  cpcoll2d  40044  mnuprdlem3  40059  dvconstbi  40156  expgrowth  40157  wessf1ornlem  40938  rnmptlb  41008  rnmptbdd  41010  rnmptbd2  41015  rnmptbd  41022  rexabsle  41189  uzub  41201  infrpgernmpt  41237  limcperiod  41405  limsupre  41418  limsupref  41462  limsupbnd1f  41463  climinfmpt  41492  limsupubuzmpt  41496  limsupmnf  41498  limsupre2  41502  limsupmnfuzlem  41503  limsupmnfuz  41504  limsupre2mpt  41507  limsupre3  41510  limsupre3mpt  41511  limsupre3uz  41513  limsupreuz  41514  limsupreuzmpt  41516  supcnvlimsup  41517  climuz  41521  lmbr3  41524  climrescn  41525  limsuplt2  41530  liminflelimsup  41553  limsupgt  41555  liminfreuz  41580  liminflt  41582  xlimpnfxnegmnf  41591  xlimmnf  41618  xlimpnf  41619  xlimmnfmpt  41620  xlimpnfmpt  41621  dfxlim2  41625  cncfshiftioo  41670  itgiccshift  41760  itgperiod  41761  fourierdlem42  41930  fourierdlem48  41935  fourierdlem81  41968  fourierdlem92  41979  fourierdlem96  41983  fourierdlem97  41984  fourierdlem98  41985  fourierdlem99  41986  fourierdlem105  41992  fourierdlem108  41995  fourierdlem110  41997  fourierdlem112  41999  fourierdlem113  42000  meaiuninc3v  42262  hoidmvval0  42365  ovnhoi  42381  ovolval5lem3  42432  ovolval5  42433  smfsup  42584  smfinflem  42587  smfinf  42588  2reuimp0  42783  fmtnofac2lem  43166  2zlidl  43637  2zrngamgm  43642  2zrngagrp  43646  2zrngmmgm  43649  eenglngeehlnmlem1  44159