Theorem cbvrexvw 3450

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3453 with a disjoint variable condition, which does not require ax-10 2145, ax-11 2161, ax-12 2177, ax-13 2390. (Contributed by NM, 2-Jun-1998.) (Revised by Gino Giotto, 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 2895	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2044	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3144	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3144	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 305	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-clel 2893  df-rex 3144

This theorem is referenced by:  cbvrex2vw  3462  reu7  3723  disjiund  5056  reusv3  5306  xpdifid  6025  fliftfun  7065  funcnvuni  7636  fiunlem  7643  nneob  8279  pssnn  8736  frfi  8763  finsschain  8831  marypha1lem  8897  supmo  8916  suplub2  8925  infmo  8959  ordtypelem3  8984  ordtypelem9  8990  wemaplem1  9010  brwdom3  9046  unwdomg  9048  cantnf  9156  trcl  9170  infxpenc2  9448  aceq2  9545  dfac5lem4  9552  kmlem9  9584  kmlem14  9589  fin23lem26  9747  fin1a2lem13  9834  axdc3lem3  9874  winainflem  10115  axgroth4  10254  suprlub  11605  supaddc  11608  supadd  11609  supmul1  11610  supmullem1  11611  supmullem2  11612  supmul  11613  ublbneg  12334  zsupss  12338  xrsupsslem  12701  xrinfmsslem  12702  rexanre  14706  rexuzre  14712  rexico  14713  caurcvg2  15034  caucvgb  15036  summolem2  15073  summo  15074  mertens  15242  prodmolem2  15289  prodmo  15290  odd2np1lem  15689  gcdcllem1  15848  pceu  16183  4sqlem12  16292  vdwlem10  16326  vdwlem13  16329  vdwnn  16334  drsdirfi  17548  grpridd  17885  smndex1mgm  18072  smndex1mndlem  18074  dfgrp2  18128  dfgrp3lem  18197  cyccom  18346  gaorb  18437  psgnunilem3  18624  psgnunilem4  18625  psgneu  18634  pj1eu  18822  efgsfo  18865  cyggeninv  19002  cygabl  19010  pgpfac1lem5  19201  pgpfac1  19202  pgpfaclem2  19204  lss1d  19735  lspsneq  19894  lspsolvlem  19914  lbsextlem2  19931  mplcoe5lem  20248  cygznlem3  20716  pmatcollpw3fi1lem2  21395  ordtrest2lem  21811  cnprest  21897  1stcfb  22053  1stcelcls  22069  elpt  22180  fbssfi  22445  fgcl  22486  rnelfmlem  22560  fmfnfmlem3  22564  txflf  22614  alexsubb  22654  alexsubALTlem4  22658  isucn2  22888  icccmplem2  23431  ply1divex  24730  coeeu  24815  plydivex  24886  aannenlem2  24918  ulmcau  24983  ulmbdd  24986  dchrptlem2  25841  bposlem9  25868  2lgslem1b  25968  pntibndlem3  26168  pntlemi  26180  pntlemp  26186  pntleml  26187  pnt3  26188  legval  26370  legov  26371  legov2  26372  outpasch  26541  lnopp2hpgb  26549  colopp  26555  erclwwlksym  27799  erclwwlktr  27800  erclwwlknsym  27849  erclwwlkntr  27850  eleclclwwlkn  27855  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  grpoidinvlem3  28283  ubthlem3  28649  norm1exi  29027  pjhthmo  29079  cdjreui  30209  cdj3i  30218  infxrge0glb  30489  cyc3genpm  30794  isarchi3  30816  archiabl  30827  ordtrest2NEWlem  31165  lmxrge0  31195  esumcvg  31345  esum2d  31352  eulerpartlems  31618  eulerpartlemgvv  31634  connpconn  32482  cvmlift2lem12  32561  cvmlift2lem13  32562  cvmlift3lem2  32567  cvmlift3lem7  32572  cvmlift3  32575  fmlasuc  32633  fmla1  32634  satffunlem1lem1  32649  satffunlem2lem1  32651  poseq  33095  soseq  33096  noprefixmo  33202  nosupdm  33204  nosupfv  33206  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem4  33211  funtransport  33492  funray  33601  funline  33603  fnessref  33705  neibastop2  33709  dissneqlem  34624  dissneq  34625  pibt2  34701  ptrest  34906  poimirlem27  34934  poimirlem32  34939  ismblfin  34948  volsupnfl  34952  itg2addnclem  34958  unirep  35003  filbcmb  35030  sdclem1  35033  sdc  35034  fdc  35035  incsequz  35038  heibor1lem  35102  heiborlem10  35113  isgrpda  35248  isdrngo2  35251  prnc  35360  prtlem13  36019  prtlem15  36026  lshpsmreu  36260  lshpkrlem1  36261  lshpkrlem3  36263  pclfinN  37051  4atex  37227  dihglblem2N  38445  lcfl7N  38652  lcf1o  38702  mzpcompact2lem  39397  eldioph3  39412  diophrex  39421  rexrabdioph  39440  eldioph4i  39458  aomclem8  39710  hbtlem2  39773  rngunsnply  39822  iunrelexpuztr  40113  ntrclsneine0lem  40463  rexlimddvcbvw  40608  cpcoll2d  40644  mnuprdlem3  40659  dvconstbi  40715  expgrowth  40716  wessf1ornlem  41494  rnmptlb  41563  rnmptbdd  41565  rnmptbd2  41570  rnmptbd  41577  rexabsle  41742  uzub  41754  infrpgernmpt  41790  limcperiod  41958  limsupre  41971  limsupbnd1f  42016  climinf2  42037  climinfmpt  42045  limsupubuzmpt  42049  limsupmnf  42051  limsupre2  42055  limsupmnfuzlem  42056  limsupmnfuz  42057  limsupre2mpt  42060  limsupre3  42063  limsupre3mpt  42064  limsupre3uz  42066  limsupreuz  42067  limsupreuzmpt  42069  supcnvlimsup  42070  climuz  42074  lmbr3  42077  climrescn  42078  limsuplt2  42083  liminflelimsup  42106  limsupgt  42108  liminfreuz  42133  liminflt  42135  xlimpnfxnegmnf  42144  xlimmnf  42171  xlimpnf  42172  xlimmnfmpt  42173  xlimpnfmpt  42174  dfxlim2  42178  cncfshiftioo  42224  itgiccshift  42314  itgperiod  42315  fourierdlem42  42483  fourierdlem48  42488  fourierdlem81  42521  fourierdlem92  42532  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem105  42545  fourierdlem108  42548  fourierdlem110  42550  fourierdlem112  42552  fourierdlem113  42553  meaiunincf  42814  meaiuninc3v  42815  hoidmvval0  42918  ovnhoi  42934  ovolval5lem3  42985  ovolval5  42986  smfsup  43137  smfinflem  43140  smfinf  43141  2reuimp0  43362  imaelsetpreimafv  43604  imasetpreimafvbijlemfo  43614  fundcmpsurinj  43618  fundcmpsurbijinj  43619  fmtnofac2lem  43779  2zlidl  44254  2zrngamgm  44259  2zrngagrp  44263  2zrngmmgm  44266  eenglngeehlnmlem1  44773