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 2142, ax-11 2158, ax-12 2178, ax-13 2377. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2377. (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 2818	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2037	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3062	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3062	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2810  df-rex 3062

This theorem is referenced by:  cbvrex2vw  3229  reu7  3720  cbviunv  5021  disjiund  5115  reusv3  5380  xpdifid  6162  fliftfun  7310  funcnvuni  7933  fiunlem  7945  poseq  8162  soseq  8163  nneob  8673  coflton  8688  cofon1  8689  cofon2  8690  pssnn  9187  frfi  9298  finsschain  9376  marypha1lem  9450  supmo  9469  suplub2  9478  infmo  9514  ordtypelem3  9539  ordtypelem9  9545  wemaplem1  9565  brwdom3  9601  unwdomg  9603  cantnf  9712  ttrcltr  9735  trcl  9747  infxpenc2  10041  aceq2  10138  dfac5lem4  10145  dfac5lem4OLD  10147  kmlem9  10178  kmlem14  10183  fin23lem26  10344  fin1a2lem13  10431  axdc3lem3  10471  winainflem  10712  axgroth4  10851  suprlub  12211  supaddc  12214  supadd  12215  supmul1  12216  supmullem1  12217  supmullem2  12218  supmul  12219  ublbneg  12954  zsupss  12958  xrsupsslem  13328  xrinfmsslem  13329  rexanre  15370  rexuzre  15376  rexico  15377  caurcvg2  15699  caucvgb  15701  summolem2  15737  summo  15738  mertens  15907  prodmolem2  15956  prodmo  15957  odd2np1lem  16364  gcdcllem1  16523  prmdvdsncoprmbd  16751  pceu  16871  4sqlem12  16981  vdwlem10  17015  vdwlem13  17018  vdwnn  17023  drsdirfi  18322  grprida  18658  smndex1mgm  18890  smndex1mndlem  18892  dfgrp2  18950  dfgrp3lem  19026  cyccom  19191  gaorb  19295  psgnunilem3  19482  psgnunilem4  19483  psgneu  19492  pj1eu  19682  efgsfo  19725  cyggeninv  19869  cygabl  19877  pgpfac1lem5  20067  pgpfac1  20068  pgpfaclem2  20070  lss1d  20925  lspsneq  21088  lspsolvlem  21108  lbsextlem2  21125  cygznlem3  21535  mplcoe5lem  22002  pmatcollpw3fi1lem2  22730  ordtrest2lem  23146  cnprest  23232  1stcfb  23388  1stcelcls  23404  elpt  23515  fbssfi  23780  fgcl  23821  rnelfmlem  23895  fmfnfmlem3  23899  txflf  23949  alexsubb  23989  alexsubALTlem4  23993  isucn2  24222  icccmplem2  24768  ply1divex  26099  coeeu  26187  plydivex  26262  aannenlem2  26294  ulmcau  26361  ulmbdd  26364  dchrptlem2  27233  bposlem9  27260  2lgslem1b  27360  pntibndlem3  27560  pntlemi  27572  pntlemp  27578  pntleml  27579  pnt3  27580  nosupprefixmo  27669  noinfprefixmo  27670  nosupcbv  27671  nosupdm  27673  nosupfv  27675  nosupres  27676  nosupbnd1lem1  27677  nosupbnd1lem4  27680  noinfcbv  27686  noinfdm  27688  noinfbnd1lem4  27695  cofsslt  27883  coinitsslt  27884  addsval2  27927  addscut  27942  addsunif  27966  norecdiv  28150  recsne0  28152  bdayn0sf1o  28316  dfnns2  28318  n0seo  28364  pw2recs  28380  recut  28404  readdscl  28407  legval  28568  legov  28569  legov2  28570  outpasch  28739  lnopp2hpgb  28747  colopp  28753  erclwwlksym  30007  erclwwlktr  30008  erclwwlknsym  30056  erclwwlkntr  30057  eleclclwwlkn  30062  hashecclwwlkn1  30063  umgrhashecclwwlk  30064  grpoidinvlem3  30492  ubthlem3  30858  norm1exi  31236  pjhthmo  31288  cdjreui  32418  cdj3i  32427  infxrge0glb  32747  mndlrinvb  33025  gsumwrd2dccatlem  33065  cyc3genpm  33168  isarchi3  33190  archiabl  33201  erler  33265  isdrng4  33294  1arithidomlem1  33555  1arithidom  33557  1arithufdlem2  33565  1arithufdlem3  33566  1arithufd  33568  fldext2chn  33767  constrconj  33784  constrextdg2lem  33787  constrextdg2  33788  constrfiss  33790  zarclsun  33906  ordtrest2NEWlem  33958  lmxrge0  33988  esumcvg  34122  esum2d  34129  eulerpartlems  34397  eulerpartlemgvv  34413  connpconn  35262  cvmlift2lem12  35341  cvmlift2lem13  35342  cvmlift3lem2  35347  cvmlift3lem7  35352  cvmlift3  35355  fmlasuc  35413  fmla1  35414  satffunlem1lem1  35429  satffunlem2lem1  35431  r1peuqusdeg1  35670  funtransport  36054  funray  36163  funline  36165  fnessref  36380  neibastop2  36384  dissneqlem  37363  dissneq  37364  pibt2  37440  ptrest  37648  poimirlem27  37676  poimirlem32  37681  ismblfin  37690  volsupnfl  37694  itg2addnclem  37700  unirep  37743  filbcmb  37769  sdclem1  37772  sdc  37773  fdc  37774  incsequz  37777  heibor1lem  37838  heiborlem10  37849  isgrpda  37984  isdrngo2  37987  prnc  38096  prtlem13  38891  prtlem15  38898  lshpsmreu  39132  lshpkrlem1  39133  lshpkrlem3  39135  pclfinN  39924  4atex  40100  dihglblem2N  41318  lcfl7N  41525  lcf1o  41575  supinf  42260  fimgmcyclem  42531  mzpcompact2lem  42749  eldioph3  42764  diophrex  42773  rexrabdioph  42792  eldioph4i  42810  aomclem8  43060  hbtlem2  43123  rngunsnply  43168  onsucrn  43270  iunrelexpuztr  43718  ntrclsneine0lem  44063  rexlimddvcbvw  44205  cpcoll2d  44258  mnuprdlem3  44273  dvconstbi  44333  expgrowth  44334  wessf1ornlem  45189  rnmptlb  45247  rnmptbdd  45249  rnmptbd2  45253  rnmptbd  45260  rexabsle  45426  uzub  45438  infrpgernmpt  45472  limcperiod  45637  limsupre  45650  limsupbnd1f  45695  climinf2  45716  climinfmpt  45724  limsupubuzmpt  45728  limsupmnf  45730  limsupre2  45734  limsupmnfuzlem  45735  limsupmnfuz  45736  limsupre2mpt  45739  limsupre3  45742  limsupre3mpt  45743  limsupre3uz  45745  limsupreuz  45746  limsupreuzmpt  45748  supcnvlimsup  45749  climuz  45753  lmbr3  45756  climrescn  45757  limsuplt2  45762  liminflelimsup  45785  limsupgt  45787  liminfreuz  45812  liminflt  45814  xlimpnfxnegmnf  45823  xlimmnf  45850  xlimpnf  45851  xlimmnfmpt  45852  xlimpnfmpt  45853  dfxlim2  45857  cncfshiftioo  45901  itgiccshift  45989  itgperiod  45990  fourierdlem42  46158  fourierdlem48  46163  fourierdlem81  46196  fourierdlem92  46207  fourierdlem96  46211  fourierdlem97  46212  fourierdlem98  46213  fourierdlem99  46214  fourierdlem105  46220  fourierdlem108  46223  fourierdlem110  46225  fourierdlem112  46227  fourierdlem113  46228  meaiunincf  46492  meaiuninc3v  46493  hoidmvval0  46596  ovnhoi  46612  ovolval5lem3  46663  ovolval5  46664  smfsup  46823  smfinflem  46826  smfinf  46827  fsetsnfo  47062  2reuimp0  47123  imaelsetpreimafv  47389  imasetpreimafvbijlemfo  47399  fundcmpsurinj  47403  fundcmpsurbijinj  47404  fmtnofac2lem  47562  2zlidl  48195  2zrngamgm  48200  2zrngagrp  48204  2zrngmmgm  48207  eenglngeehlnmlem1  48697  upciclem4  49084