Theorem cbvrexvw 3362

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3365 with a disjoint variable condition, which does not require ax-10 2142, ax-11 2158, ax-12 2175, ax-13 2379. (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 2834	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2044	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3076	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3076	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3071

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 1911  ax-6 1970  ax-7 2015  ax-8 2113

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2830  df-rex 3076

This theorem is referenced by:  cbvrex2vw  3374  reu7  3648  disjiund  5026  reusv3  5278  xpdifid  6002  fliftfun  7065  funcnvuni  7647  fiunlem  7653  nneob  8295  pssnn  8751  pssnnOLD  8787  frfi  8809  finsschain  8877  marypha1lem  8943  supmo  8962  suplub2  8971  infmo  9005  ordtypelem3  9030  ordtypelem9  9036  wemaplem1  9056  brwdom3  9092  unwdomg  9094  cantnf  9202  trcl  9216  infxpenc2  9495  aceq2  9592  dfac5lem4  9599  kmlem9  9631  kmlem14  9636  fin23lem26  9798  fin1a2lem13  9885  axdc3lem3  9925  winainflem  10166  axgroth4  10305  suprlub  11654  supaddc  11657  supadd  11658  supmul1  11659  supmullem1  11660  supmullem2  11661  supmul  11662  ublbneg  12386  zsupss  12390  xrsupsslem  12754  xrinfmsslem  12755  rexanre  14767  rexuzre  14773  rexico  14774  caurcvg2  15095  caucvgb  15097  summolem2  15134  summo  15135  mertens  15303  prodmolem2  15350  prodmo  15351  odd2np1lem  15754  gcdcllem1  15911  prmdvdsncoprmbd  16136  pceu  16252  4sqlem12  16361  vdwlem10  16395  vdwlem13  16398  vdwnn  16403  drsdirfi  17628  grpridd  17965  smndex1mgm  18152  smndex1mndlem  18154  dfgrp2  18209  dfgrp3lem  18278  cyccom  18427  gaorb  18518  psgnunilem3  18705  psgnunilem4  18706  psgneu  18715  pj1eu  18903  efgsfo  18946  cyggeninv  19084  cygabl  19092  pgpfac1lem5  19283  pgpfac1  19284  pgpfaclem2  19286  lss1d  19817  lspsneq  19976  lspsolvlem  19996  lbsextlem2  20013  cygznlem3  20351  mplcoe5lem  20813  pmatcollpw3fi1lem2  21501  ordtrest2lem  21917  cnprest  22003  1stcfb  22159  1stcelcls  22175  elpt  22286  fbssfi  22551  fgcl  22592  rnelfmlem  22666  fmfnfmlem3  22670  txflf  22720  alexsubb  22760  alexsubALTlem4  22764  isucn2  22994  icccmplem2  23538  ply1divex  24850  coeeu  24935  plydivex  25006  aannenlem2  25038  ulmcau  25103  ulmbdd  25106  dchrptlem2  25962  bposlem9  25989  2lgslem1b  26089  pntibndlem3  26289  pntlemi  26301  pntlemp  26307  pntleml  26308  pnt3  26309  legval  26491  legov  26492  legov2  26493  outpasch  26662  lnopp2hpgb  26670  colopp  26676  erclwwlksym  27919  erclwwlktr  27920  erclwwlknsym  27968  erclwwlkntr  27969  eleclclwwlkn  27974  hashecclwwlkn1  27975  umgrhashecclwwlk  27976  grpoidinvlem3  28402  ubthlem3  28768  norm1exi  29146  pjhthmo  29198  cdjreui  30328  cdj3i  30337  infxrge0glb  30625  cyc3genpm  30958  isarchi3  30980  archiabl  30991  zarclsun  31354  ordtrest2NEWlem  31406  lmxrge0  31436  esumcvg  31586  esum2d  31593  eulerpartlems  31859  eulerpartlemgvv  31875  connpconn  32726  cvmlift2lem12  32805  cvmlift2lem13  32806  cvmlift3lem2  32811  cvmlift3lem7  32816  cvmlift3  32819  fmlasuc  32877  fmla1  32878  satffunlem1lem1  32893  satffunlem2lem1  32895  poseq  33370  soseq  33371  nosupprefixmo  33501  noinfprefixmo  33502  nosupcbv  33503  nosupdm  33505  nosupfv  33507  nosupres  33508  nosupbnd1lem1  33509  nosupbnd1lem4  33512  noinfcbv  33518  noinfdm  33520  noinfbnd1lem4  33527  funtransport  33917  funray  34026  funline  34028  fnessref  34130  neibastop2  34134  dissneqlem  35072  dissneq  35073  pibt2  35149  ptrest  35371  poimirlem27  35399  poimirlem32  35404  ismblfin  35413  volsupnfl  35417  itg2addnclem  35423  unirep  35466  filbcmb  35493  sdclem1  35496  sdc  35497  fdc  35498  incsequz  35501  heibor1lem  35562  heiborlem10  35573  isgrpda  35708  isdrngo2  35711  prnc  35820  prtlem13  36479  prtlem15  36486  lshpsmreu  36720  lshpkrlem1  36721  lshpkrlem3  36723  pclfinN  37511  4atex  37687  dihglblem2N  38905  lcfl7N  39112  lcf1o  39162  mzpcompact2lem  40110  eldioph3  40125  diophrex  40134  rexrabdioph  40153  eldioph4i  40171  aomclem8  40423  hbtlem2  40486  rngunsnply  40535  iunrelexpuztr  40838  ntrclsneine0lem  41185  rexlimddvcbvw  41330  cpcoll2d  41385  mnuprdlem3  41400  dvconstbi  41456  expgrowth  41457  wessf1ornlem  42226  rnmptlb  42293  rnmptbdd  42295  rnmptbd2  42300  rnmptbd  42307  rexabsle  42467  uzub  42479  infrpgernmpt  42515  limcperiod  42681  limsupre  42694  limsupbnd1f  42739  climinf2  42760  climinfmpt  42768  limsupubuzmpt  42772  limsupmnf  42774  limsupre2  42778  limsupmnfuzlem  42779  limsupmnfuz  42780  limsupre2mpt  42783  limsupre3  42786  limsupre3mpt  42787  limsupre3uz  42789  limsupreuz  42790  limsupreuzmpt  42792  supcnvlimsup  42793  climuz  42797  lmbr3  42800  climrescn  42801  limsuplt2  42806  liminflelimsup  42829  limsupgt  42831  liminfreuz  42856  liminflt  42858  xlimpnfxnegmnf  42867  xlimmnf  42894  xlimpnf  42895  xlimmnfmpt  42896  xlimpnfmpt  42897  dfxlim2  42901  cncfshiftioo  42945  itgiccshift  43033  itgperiod  43034  fourierdlem42  43202  fourierdlem48  43207  fourierdlem81  43240  fourierdlem92  43251  fourierdlem96  43255  fourierdlem97  43256  fourierdlem98  43257  fourierdlem99  43258  fourierdlem105  43264  fourierdlem108  43267  fourierdlem110  43269  fourierdlem112  43271  fourierdlem113  43272  meaiunincf  43533  meaiuninc3v  43534  hoidmvval0  43637  ovnhoi  43653  ovolval5lem3  43704  ovolval5  43705  smfsup  43856  smfinflem  43859  smfinf  43860  fsetsnfo  44055  2reuimp0  44097  imaelsetpreimafv  44339  imasetpreimafvbijlemfo  44349  fundcmpsurinj  44353  fundcmpsurbijinj  44354  fmtnofac2lem  44512  2zlidl  44984  2zrngamgm  44989  2zrngagrp  44993  2zrngmmgm  44996  eenglngeehlnmlem1  45575