Theorem cbvrexvw 3225

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3349 with a disjoint variable condition, which does not require ax-10 2140, ax-11 2156, ax-12 2176, ax-13 2375. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2375. (Revised by GG, 10-Jan-2024.)

Hypothesis

Ref	Expression
cbvralvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrexvw	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

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

Proof of Theorem cbvrexvw

Step	Hyp	Ref	Expression
1		eleq1w 2816	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2035	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3060	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3060	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1778   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2808  df-rex 3060

This theorem is referenced by:  cbvrex2vw  3229  reu7  3722  cbviunv  5022  disjiund  5116  reusv3  5387  xpdifid  6170  fliftfun  7315  funcnvuni  7937  fiunlem  7949  poseq  8166  soseq  8167  nneob  8677  coflton  8692  cofon1  8693  cofon2  8694  pssnn  9191  frfi  9304  finsschain  9382  marypha1lem  9456  supmo  9475  suplub2  9484  infmo  9518  ordtypelem3  9543  ordtypelem9  9549  wemaplem1  9569  brwdom3  9605  unwdomg  9607  cantnf  9716  ttrcltr  9739  trcl  9751  infxpenc2  10045  aceq2  10142  dfac5lem4  10149  dfac5lem4OLD  10151  kmlem9  10182  kmlem14  10187  fin23lem26  10348  fin1a2lem13  10435  axdc3lem3  10475  winainflem  10716  axgroth4  10855  suprlub  12215  supaddc  12218  supadd  12219  supmul1  12220  supmullem1  12221  supmullem2  12222  supmul  12223  ublbneg  12958  zsupss  12962  xrsupsslem  13332  xrinfmsslem  13333  rexanre  15368  rexuzre  15374  rexico  15375  caurcvg2  15697  caucvgb  15699  summolem2  15735  summo  15736  mertens  15905  prodmolem2  15954  prodmo  15955  odd2np1lem  16360  gcdcllem1  16519  prmdvdsncoprmbd  16747  pceu  16867  4sqlem12  16977  vdwlem10  17011  vdwlem13  17014  vdwnn  17019  drsdirfi  18326  grprida  18662  smndex1mgm  18894  smndex1mndlem  18896  dfgrp2  18954  dfgrp3lem  19030  cyccom  19195  gaorb  19299  psgnunilem3  19487  psgnunilem4  19488  psgneu  19497  pj1eu  19687  efgsfo  19730  cyggeninv  19874  cygabl  19882  pgpfac1lem5  20072  pgpfac1  20073  pgpfaclem2  20075  lss1d  20934  lspsneq  21097  lspsolvlem  21117  lbsextlem2  21134  cygznlem3  21555  mplcoe5lem  22024  pmatcollpw3fi1lem2  22760  ordtrest2lem  23176  cnprest  23262  1stcfb  23418  1stcelcls  23434  elpt  23545  fbssfi  23810  fgcl  23851  rnelfmlem  23925  fmfnfmlem3  23929  txflf  23979  alexsubb  24019  alexsubALTlem4  24023  isucn2  24252  icccmplem2  24800  ply1divex  26131  coeeu  26219  plydivex  26294  aannenlem2  26326  ulmcau  26393  ulmbdd  26396  dchrptlem2  27264  bposlem9  27291  2lgslem1b  27391  pntibndlem3  27591  pntlemi  27603  pntlemp  27609  pntleml  27610  pnt3  27611  nosupprefixmo  27700  noinfprefixmo  27701  nosupcbv  27702  nosupdm  27704  nosupfv  27706  nosupres  27707  nosupbnd1lem1  27708  nosupbnd1lem4  27711  noinfcbv  27717  noinfdm  27719  noinfbnd1lem4  27726  cofsslt  27907  coinitsslt  27908  addsval2  27951  addscut  27966  addsunif  27990  norecdiv  28171  dfnns2  28317  n0seo  28360  recut  28383  readdscl  28386  legval  28547  legov  28548  legov2  28549  outpasch  28718  lnopp2hpgb  28726  colopp  28732  erclwwlksym  29987  erclwwlktr  29988  erclwwlknsym  30036  erclwwlkntr  30037  eleclclwwlkn  30042  hashecclwwlkn1  30043  umgrhashecclwwlk  30044  grpoidinvlem3  30472  ubthlem3  30838  norm1exi  31216  pjhthmo  31268  cdjreui  32398  cdj3i  32407  infxrge0glb  32716  mndlrinvb  32976  gsumwrd2dccatlem  33015  cyc3genpm  33118  isarchi3  33140  archiabl  33151  erler  33215  isdrng4  33244  1arithidomlem1  33504  1arithidom  33506  1arithufdlem2  33514  1arithufdlem3  33515  1arithufd  33517  fldext2chn  33710  constrconj  33727  constrextdg2lem  33730  constrextdg2  33731  zarclsun  33810  ordtrest2NEWlem  33862  lmxrge0  33892  esumcvg  34028  esum2d  34035  eulerpartlems  34303  eulerpartlemgvv  34319  connpconn  35181  cvmlift2lem12  35260  cvmlift2lem13  35261  cvmlift3lem2  35266  cvmlift3lem7  35271  cvmlift3  35274  fmlasuc  35332  fmla1  35333  satffunlem1lem1  35348  satffunlem2lem1  35350  r1peuqusdeg1  35589  funtransport  35973  funray  36082  funline  36084  fnessref  36299  neibastop2  36303  dissneqlem  37282  dissneq  37283  pibt2  37359  ptrest  37567  poimirlem27  37595  poimirlem32  37600  ismblfin  37609  volsupnfl  37613  itg2addnclem  37619  unirep  37662  filbcmb  37688  sdclem1  37691  sdc  37692  fdc  37693  incsequz  37696  heibor1lem  37757  heiborlem10  37768  isgrpda  37903  isdrngo2  37906  prnc  38015  prtlem13  38810  prtlem15  38817  lshpsmreu  39051  lshpkrlem1  39052  lshpkrlem3  39054  pclfinN  39843  4atex  40019  dihglblem2N  41237  lcfl7N  41444  lcf1o  41494  supinf  42223  fimgmcyclem  42488  mzpcompact2lem  42707  eldioph3  42722  diophrex  42731  rexrabdioph  42750  eldioph4i  42768  aomclem8  43018  hbtlem2  43081  rngunsnply  43126  onsucrn  43229  iunrelexpuztr  43677  ntrclsneine0lem  44022  rexlimddvcbvw  44164  cpcoll2d  44223  mnuprdlem3  44238  dvconstbi  44298  expgrowth  44299  wessf1ornlem  45135  rnmptlb  45195  rnmptbdd  45197  rnmptbd2  45201  rnmptbd  45208  rexabsle  45375  uzub  45387  infrpgernmpt  45421  limcperiod  45588  limsupre  45601  limsupbnd1f  45646  climinf2  45667  climinfmpt  45675  limsupubuzmpt  45679  limsupmnf  45681  limsupre2  45685  limsupmnfuzlem  45686  limsupmnfuz  45687  limsupre2mpt  45690  limsupre3  45693  limsupre3mpt  45694  limsupre3uz  45696  limsupreuz  45697  limsupreuzmpt  45699  supcnvlimsup  45700  climuz  45704  lmbr3  45707  climrescn  45708  limsuplt2  45713  liminflelimsup  45736  limsupgt  45738  liminfreuz  45763  liminflt  45765  xlimpnfxnegmnf  45774  xlimmnf  45801  xlimpnf  45802  xlimmnfmpt  45803  xlimpnfmpt  45804  dfxlim2  45808  cncfshiftioo  45852  itgiccshift  45940  itgperiod  45941  fourierdlem42  46109  fourierdlem48  46114  fourierdlem81  46147  fourierdlem92  46158  fourierdlem96  46162  fourierdlem97  46163  fourierdlem98  46164  fourierdlem99  46165  fourierdlem105  46171  fourierdlem108  46174  fourierdlem110  46176  fourierdlem112  46178  fourierdlem113  46179  meaiunincf  46443  meaiuninc3v  46444  hoidmvval0  46547  ovnhoi  46563  ovolval5lem3  46614  ovolval5  46615  smfsup  46774  smfinflem  46777  smfinf  46778  fsetsnfo  47011  2reuimp0  47072  imaelsetpreimafv  47328  imasetpreimafvbijlemfo  47338  fundcmpsurinj  47342  fundcmpsurbijinj  47343  fmtnofac2lem  47501  2zlidl  48102  2zrngamgm  48107  2zrngagrp  48111  2zrngmmgm  48114  eenglngeehlnmlem1  48604  upciclem4  48885