Theorem cbvrexvw 3385

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3390 with a disjoint variable condition, which does not require ax-10 2138, ax-11 2155, ax-12 2172, ax-13 2373. (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 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2041	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3071	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

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

This theorem is referenced by:  cbvrex2vw  3398  reu7  3668  disjiund  5065  reusv3  5329  xpdifid  6076  fliftfun  7192  funcnvuni  7787  fiunlem  7793  nneob  8495  pssnn  8960  pssnnOLD  9049  frfi  9068  finsschain  9135  marypha1lem  9201  supmo  9220  suplub2  9229  infmo  9263  ordtypelem3  9288  ordtypelem9  9294  wemaplem1  9314  brwdom3  9350  unwdomg  9352  cantnf  9460  ttrcltr  9483  trcl  9495  infxpenc2  9787  aceq2  9884  dfac5lem4  9891  kmlem9  9923  kmlem14  9928  fin23lem26  10090  fin1a2lem13  10177  axdc3lem3  10217  winainflem  10458  axgroth4  10597  suprlub  11948  supaddc  11951  supadd  11952  supmul1  11953  supmullem1  11954  supmullem2  11955  supmul  11956  ublbneg  12682  zsupss  12686  xrsupsslem  13050  xrinfmsslem  13051  rexanre  15067  rexuzre  15073  rexico  15074  caurcvg2  15398  caucvgb  15400  summolem2  15437  summo  15438  mertens  15607  prodmolem2  15654  prodmo  15655  odd2np1lem  16058  gcdcllem1  16215  prmdvdsncoprmbd  16440  pceu  16556  4sqlem12  16666  vdwlem10  16700  vdwlem13  16703  vdwnn  16708  drsdirfi  18032  grpridd  18368  smndex1mgm  18555  smndex1mndlem  18557  dfgrp2  18613  dfgrp3lem  18682  cyccom  18831  gaorb  18922  psgnunilem3  19113  psgnunilem4  19114  psgneu  19123  pj1eu  19311  efgsfo  19354  cyggeninv  19492  cygabl  19500  pgpfac1lem5  19691  pgpfac1  19692  pgpfaclem2  19694  lss1d  20234  lspsneq  20393  lspsolvlem  20413  lbsextlem2  20430  cygznlem3  20786  mplcoe5lem  21249  pmatcollpw3fi1lem2  21945  ordtrest2lem  22363  cnprest  22449  1stcfb  22605  1stcelcls  22621  elpt  22732  fbssfi  22997  fgcl  23038  rnelfmlem  23112  fmfnfmlem3  23116  txflf  23166  alexsubb  23206  alexsubALTlem4  23210  isucn2  23440  icccmplem2  23995  ply1divex  25310  coeeu  25395  plydivex  25466  aannenlem2  25498  ulmcau  25563  ulmbdd  25566  dchrptlem2  26422  bposlem9  26449  2lgslem1b  26549  pntibndlem3  26749  pntlemi  26761  pntlemp  26767  pntleml  26768  pnt3  26769  legval  26954  legov  26955  legov2  26956  outpasch  27125  lnopp2hpgb  27133  colopp  27139  erclwwlksym  28394  erclwwlktr  28395  erclwwlknsym  28443  erclwwlkntr  28444  eleclclwwlkn  28449  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  grpoidinvlem3  28877  ubthlem3  29243  norm1exi  29621  pjhthmo  29673  cdjreui  30803  cdj3i  30812  infxrge0glb  31097  cyc3genpm  31428  isarchi3  31450  archiabl  31461  zarclsun  31829  ordtrest2NEWlem  31881  lmxrge0  31911  esumcvg  32063  esum2d  32070  eulerpartlems  32336  eulerpartlemgvv  32352  connpconn  33206  cvmlift2lem12  33285  cvmlift2lem13  33286  cvmlift3lem2  33291  cvmlift3lem7  33296  cvmlift3  33299  fmlasuc  33357  fmla1  33358  satffunlem1lem1  33373  satffunlem2lem1  33375  poseq  33811  soseq  33812  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupdm  33916  nosupfv  33918  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem4  33923  noinfcbv  33929  noinfdm  33931  noinfbnd1lem4  33938  cofsslt  34097  coinitsslt  34098  funtransport  34342  funray  34451  funline  34453  fnessref  34555  neibastop2  34559  dissneqlem  35520  dissneq  35521  pibt2  35597  ptrest  35785  poimirlem27  35813  poimirlem32  35818  ismblfin  35827  volsupnfl  35831  itg2addnclem  35837  unirep  35880  filbcmb  35907  sdclem1  35910  sdc  35911  fdc  35912  incsequz  35915  heibor1lem  35976  heiborlem10  35987  isgrpda  36122  isdrngo2  36125  prnc  36234  prtlem13  36889  prtlem15  36896  lshpsmreu  37130  lshpkrlem1  37131  lshpkrlem3  37133  pclfinN  37921  4atex  38097  dihglblem2N  39315  lcfl7N  39522  lcf1o  39572  mzpcompact2lem  40580  eldioph3  40595  diophrex  40604  rexrabdioph  40623  eldioph4i  40641  aomclem8  40893  hbtlem2  40956  rngunsnply  41005  iunrelexpuztr  41334  ntrclsneine0lem  41681  rexlimddvcbvw  41824  cpcoll2d  41884  mnuprdlem3  41899  dvconstbi  41959  expgrowth  41960  wessf1ornlem  42729  rnmptlb  42795  rnmptbdd  42797  rnmptbd2  42802  rnmptbd  42809  rexabsle  42966  uzub  42978  infrpgernmpt  43012  limcperiod  43176  limsupre  43189  limsupbnd1f  43234  climinf2  43255  climinfmpt  43263  limsupubuzmpt  43267  limsupmnf  43269  limsupre2  43273  limsupmnfuzlem  43274  limsupmnfuz  43275  limsupre2mpt  43278  limsupre3  43281  limsupre3mpt  43282  limsupre3uz  43284  limsupreuz  43285  limsupreuzmpt  43287  supcnvlimsup  43288  climuz  43292  lmbr3  43295  climrescn  43296  limsuplt2  43301  liminflelimsup  43324  limsupgt  43326  liminfreuz  43351  liminflt  43353  xlimpnfxnegmnf  43362  xlimmnf  43389  xlimpnf  43390  xlimmnfmpt  43391  xlimpnfmpt  43392  dfxlim2  43396  cncfshiftioo  43440  itgiccshift  43528  itgperiod  43529  fourierdlem42  43697  fourierdlem48  43702  fourierdlem81  43735  fourierdlem92  43746  fourierdlem96  43750  fourierdlem97  43751  fourierdlem98  43752  fourierdlem99  43753  fourierdlem105  43759  fourierdlem108  43762  fourierdlem110  43764  fourierdlem112  43766  fourierdlem113  43767  meaiunincf  44028  meaiuninc3v  44029  hoidmvval0  44132  ovnhoi  44148  ovolval5lem3  44199  ovolval5  44200  smfsup  44358  smfinflem  44361  smfinf  44362  fsetsnfo  44558  2reuimp0  44617  imaelsetpreimafv  44858  imasetpreimafvbijlemfo  44868  fundcmpsurinj  44872  fundcmpsurbijinj  44873  fmtnofac2lem  45031  2zlidl  45503  2zrngamgm  45508  2zrngagrp  45512  2zrngmmgm  45515  eenglngeehlnmlem1  46094