Theorem cbvrexvw 3235

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3361 with a disjoint variable condition, which does not require ax-10 2137, ax-11 2154, ax-12 2171, ax-13 2371. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2371. (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 2816	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2040	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3071	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-clel 2810  df-rex 3071

This theorem is referenced by:  cbvrex2vw  3239  reu7  3728  disjiund  5138  reusv3  5403  xpdifid  6167  fliftfun  7308  funcnvuni  7921  fiunlem  7927  poseq  8143  soseq  8144  nneob  8654  coflton  8669  cofon1  8670  cofon2  8671  pssnn  9167  pssnnOLD  9264  frfi  9287  finsschain  9358  marypha1lem  9427  supmo  9446  suplub2  9455  infmo  9489  ordtypelem3  9514  ordtypelem9  9520  wemaplem1  9540  brwdom3  9576  unwdomg  9578  cantnf  9687  ttrcltr  9710  trcl  9722  infxpenc2  10016  aceq2  10113  dfac5lem4  10120  kmlem9  10152  kmlem14  10157  fin23lem26  10319  fin1a2lem13  10406  axdc3lem3  10446  winainflem  10687  axgroth4  10826  suprlub  12177  supaddc  12180  supadd  12181  supmul1  12182  supmullem1  12183  supmullem2  12184  supmul  12185  ublbneg  12916  zsupss  12920  xrsupsslem  13285  xrinfmsslem  13286  rexanre  15292  rexuzre  15298  rexico  15299  caurcvg2  15623  caucvgb  15625  summolem2  15661  summo  15662  mertens  15831  prodmolem2  15878  prodmo  15879  odd2np1lem  16282  gcdcllem1  16439  prmdvdsncoprmbd  16662  pceu  16778  4sqlem12  16888  vdwlem10  16922  vdwlem13  16925  vdwnn  16930  drsdirfi  18257  grprida  18593  smndex1mgm  18787  smndex1mndlem  18789  dfgrp2  18846  dfgrp3lem  18920  cyccom  19079  gaorb  19170  psgnunilem3  19363  psgnunilem4  19364  psgneu  19373  pj1eu  19563  efgsfo  19606  cyggeninv  19750  cygabl  19758  pgpfac1lem5  19948  pgpfac1  19949  pgpfaclem2  19951  lss1d  20573  lspsneq  20734  lspsolvlem  20754  lbsextlem2  20771  cygznlem3  21124  mplcoe5lem  21593  pmatcollpw3fi1lem2  22288  ordtrest2lem  22706  cnprest  22792  1stcfb  22948  1stcelcls  22964  elpt  23075  fbssfi  23340  fgcl  23381  rnelfmlem  23455  fmfnfmlem3  23459  txflf  23509  alexsubb  23549  alexsubALTlem4  23553  isucn2  23783  icccmplem2  24338  ply1divex  25653  coeeu  25738  plydivex  25809  aannenlem2  25841  ulmcau  25906  ulmbdd  25909  dchrptlem2  26765  bposlem9  26792  2lgslem1b  26892  pntibndlem3  27092  pntlemi  27104  pntlemp  27110  pntleml  27111  pnt3  27112  nosupprefixmo  27200  noinfprefixmo  27201  nosupcbv  27202  nosupdm  27204  nosupfv  27206  nosupres  27207  nosupbnd1lem1  27208  nosupbnd1lem4  27211  noinfcbv  27217  noinfdm  27219  noinfbnd1lem4  27226  cofsslt  27402  coinitsslt  27403  addsval2  27444  addscut  27459  addsunif  27482  norecdiv  27635  legval  27832  legov  27833  legov2  27834  outpasch  28003  lnopp2hpgb  28011  colopp  28017  erclwwlksym  29271  erclwwlktr  29272  erclwwlknsym  29320  erclwwlkntr  29321  eleclclwwlkn  29326  hashecclwwlkn1  29327  umgrhashecclwwlk  29328  grpoidinvlem3  29754  ubthlem3  30120  norm1exi  30498  pjhthmo  30550  cdjreui  31680  cdj3i  31689  infxrge0glb  31973  cyc3genpm  32306  isarchi3  32328  archiabl  32339  isdrng4  32390  zarclsun  32845  ordtrest2NEWlem  32897  lmxrge0  32927  esumcvg  33079  esum2d  33086  eulerpartlems  33354  eulerpartlemgvv  33370  connpconn  34221  cvmlift2lem12  34300  cvmlift2lem13  34301  cvmlift3lem2  34306  cvmlift3lem7  34311  cvmlift3  34314  fmlasuc  34372  fmla1  34373  satffunlem1lem1  34388  satffunlem2lem1  34390  funtransport  34998  funray  35107  funline  35109  fnessref  35237  neibastop2  35241  dissneqlem  36216  dissneq  36217  pibt2  36293  ptrest  36482  poimirlem27  36510  poimirlem32  36515  ismblfin  36524  volsupnfl  36528  itg2addnclem  36534  unirep  36577  filbcmb  36603  sdclem1  36606  sdc  36607  fdc  36608  incsequz  36611  heibor1lem  36672  heiborlem10  36683  isgrpda  36818  isdrngo2  36821  prnc  36930  prtlem13  37733  prtlem15  37740  lshpsmreu  37974  lshpkrlem1  37975  lshpkrlem3  37977  pclfinN  38766  4atex  38942  dihglblem2N  40160  lcfl7N  40367  lcf1o  40417  mzpcompact2lem  41479  eldioph3  41494  diophrex  41503  rexrabdioph  41522  eldioph4i  41540  aomclem8  41793  hbtlem2  41856  rngunsnply  41905  onsucrn  42011  iunrelexpuztr  42460  ntrclsneine0lem  42805  rexlimddvcbvw  42948  cpcoll2d  43008  mnuprdlem3  43023  dvconstbi  43083  expgrowth  43084  wessf1ornlem  43872  rnmptlb  43937  rnmptbdd  43939  rnmptbd2  43943  rnmptbd  43950  rexabsle  44119  uzub  44131  infrpgernmpt  44165  limcperiod  44334  limsupre  44347  limsupbnd1f  44392  climinf2  44413  climinfmpt  44421  limsupubuzmpt  44425  limsupmnf  44427  limsupre2  44431  limsupmnfuzlem  44432  limsupmnfuz  44433  limsupre2mpt  44436  limsupre3  44439  limsupre3mpt  44440  limsupre3uz  44442  limsupreuz  44443  limsupreuzmpt  44445  supcnvlimsup  44446  climuz  44450  lmbr3  44453  climrescn  44454  limsuplt2  44459  liminflelimsup  44482  limsupgt  44484  liminfreuz  44509  liminflt  44511  xlimpnfxnegmnf  44520  xlimmnf  44547  xlimpnf  44548  xlimmnfmpt  44549  xlimpnfmpt  44550  dfxlim2  44554  cncfshiftioo  44598  itgiccshift  44686  itgperiod  44687  fourierdlem42  44855  fourierdlem48  44860  fourierdlem81  44893  fourierdlem92  44904  fourierdlem96  44908  fourierdlem97  44909  fourierdlem98  44910  fourierdlem99  44911  fourierdlem105  44917  fourierdlem108  44920  fourierdlem110  44922  fourierdlem112  44924  fourierdlem113  44925  meaiunincf  45189  meaiuninc3v  45190  hoidmvval0  45293  ovnhoi  45309  ovolval5lem3  45360  ovolval5  45361  smfsup  45520  smfinflem  45523  smfinf  45524  fsetsnfo  45753  2reuimp0  45812  imaelsetpreimafv  46053  imasetpreimafvbijlemfo  46063  fundcmpsurinj  46067  fundcmpsurbijinj  46068  fmtnofac2lem  46226  2zlidl  46822  2zrngamgm  46827  2zrngagrp  46831  2zrngmmgm  46834  eenglngeehlnmlem1  47413