Theorem cbvrexvw 3211

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3331 with a disjoint variable condition, which does not require ax-10 2144, ax-11 2160, ax-12 2180, ax-13 2372. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2372. (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 2814	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2038	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3057	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3057	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056

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 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-rex 3057

This theorem is referenced by:  cbvrex2vw  3215  reu7  3686  cbviunv  4984  disjiund  5077  reusv3  5338  xpdifid  6110  fliftfun  7241  funcnvuni  7857  fiunlem  7869  poseq  8083  soseq  8084  nneob  8566  coflton  8581  cofon1  8582  cofon2  8583  pssnn  9073  frfi  9164  finsschain  9238  marypha1lem  9312  supmo  9331  suplub2  9340  infmo  9376  ordtypelem3  9401  ordtypelem9  9407  wemaplem1  9427  brwdom3  9463  unwdomg  9465  cantnf  9578  ttrcltr  9601  trcl  9613  infxpenc2  9908  aceq2  10005  dfac5lem4  10012  dfac5lem4OLD  10014  kmlem9  10045  kmlem14  10050  fin23lem26  10211  fin1a2lem13  10298  axdc3lem3  10338  winainflem  10579  axgroth4  10718  suprlub  12081  supaddc  12084  supadd  12085  supmul1  12086  supmullem1  12087  supmullem2  12088  supmul  12089  ublbneg  12826  zsupss  12830  xrsupsslem  13201  xrinfmsslem  13202  rexanre  15249  rexuzre  15255  rexico  15256  caurcvg2  15580  caucvgb  15582  summolem2  15618  summo  15619  mertens  15788  prodmolem2  15837  prodmo  15838  odd2np1lem  16246  gcdcllem1  16405  prmdvdsncoprmbd  16633  pceu  16753  4sqlem12  16863  vdwlem10  16897  vdwlem13  16900  vdwnn  16905  drsdirfi  18206  grprida  18578  smndex1mgm  18810  smndex1mndlem  18812  dfgrp2  18870  dfgrp3lem  18946  cyccom  19110  gaorb  19214  psgnunilem3  19403  psgnunilem4  19404  psgneu  19413  pj1eu  19603  efgsfo  19646  cyggeninv  19790  cygabl  19798  pgpfac1lem5  19988  pgpfac1  19989  pgpfaclem2  19991  lss1d  20891  lspsneq  21054  lspsolvlem  21074  lbsextlem2  21091  cygznlem3  21501  mplcoe5lem  21969  pmatcollpw3fi1lem2  22697  ordtrest2lem  23113  cnprest  23199  1stcfb  23355  1stcelcls  23371  elpt  23482  fbssfi  23747  fgcl  23788  rnelfmlem  23862  fmfnfmlem3  23866  txflf  23916  alexsubb  23956  alexsubALTlem4  23960  isucn2  24188  icccmplem2  24734  ply1divex  26064  coeeu  26152  plydivex  26227  aannenlem2  26259  ulmcau  26326  ulmbdd  26329  dchrptlem2  27198  bposlem9  27225  2lgslem1b  27325  pntibndlem3  27525  pntlemi  27537  pntlemp  27543  pntleml  27544  pnt3  27545  nosupprefixmo  27634  noinfprefixmo  27635  nosupcbv  27636  nosupdm  27638  nosupfv  27640  nosupres  27641  nosupbnd1lem1  27642  nosupbnd1lem4  27645  noinfcbv  27651  noinfdm  27653  noinfbnd1lem4  27660  cofsslt  27857  coinitsslt  27858  addsval2  27901  addscut  27916  addsunif  27940  norecdiv  28124  recsne0  28126  bdayn0sf1o  28290  dfnns2  28292  n0seo  28339  pw2recs  28356  recut  28393  readdscl  28396  legval  28557  legov  28558  legov2  28559  outpasch  28728  lnopp2hpgb  28736  colopp  28742  erclwwlksym  29993  erclwwlktr  29994  erclwwlknsym  30042  erclwwlkntr  30043  eleclclwwlkn  30048  hashecclwwlkn1  30049  umgrhashecclwwlk  30050  grpoidinvlem3  30478  ubthlem3  30844  norm1exi  31222  pjhthmo  31274  cdjreui  32404  cdj3i  32413  infxrge0glb  32740  mndlrinvb  32998  gsumwrd2dccatlem  33038  cyc3genpm  33113  isarchi3  33148  archiabl  33159  erler  33224  isdrng4  33253  1arithidomlem1  33492  1arithidom  33494  1arithufdlem2  33502  1arithufdlem3  33503  1arithufd  33505  fldext2chn  33733  constrconj  33750  constrextdg2lem  33753  constrextdg2  33754  constrfiss  33756  zarclsun  33875  ordtrest2NEWlem  33927  lmxrge0  33957  esumcvg  34091  esum2d  34098  eulerpartlems  34365  eulerpartlemgvv  34381  onvf1odlem2  35140  connpconn  35271  cvmlift2lem12  35350  cvmlift2lem13  35351  cvmlift3lem2  35356  cvmlift3lem7  35361  cvmlift3  35364  fmlasuc  35422  fmla1  35423  satffunlem1lem1  35438  satffunlem2lem1  35440  r1peuqusdeg1  35679  funtransport  36065  funray  36174  funline  36176  fnessref  36391  neibastop2  36395  dissneqlem  37374  dissneq  37375  pibt2  37451  ptrest  37659  poimirlem27  37687  poimirlem32  37692  ismblfin  37701  volsupnfl  37705  itg2addnclem  37711  unirep  37754  filbcmb  37780  sdclem1  37783  sdc  37784  fdc  37785  incsequz  37788  heibor1lem  37849  heiborlem10  37860  isgrpda  37995  isdrngo2  37998  prnc  38107  prtlem13  38907  prtlem15  38914  lshpsmreu  39148  lshpkrlem1  39149  lshpkrlem3  39151  pclfinN  39939  4atex  40115  dihglblem2N  41333  lcfl7N  41540  lcf1o  41590  supinf  42275  fimgmcyclem  42566  mzpcompact2lem  42784  eldioph3  42799  diophrex  42808  rexrabdioph  42827  eldioph4i  42845  aomclem8  43094  hbtlem2  43157  rngunsnply  43202  onsucrn  43304  iunrelexpuztr  43752  ntrclsneine0lem  44097  rexlimddvcbvw  44239  cpcoll2d  44292  mnuprdlem3  44307  dvconstbi  44367  expgrowth  44368  wessf1ornlem  45222  rnmptlb  45280  rnmptbdd  45282  rnmptbd2  45286  rnmptbd  45293  rexabsle  45457  uzub  45469  infrpgernmpt  45503  limcperiod  45668  limsupre  45679  limsupbnd1f  45724  climinf2  45745  climinfmpt  45753  limsupubuzmpt  45757  limsupmnf  45759  limsupre2  45763  limsupmnfuzlem  45764  limsupmnfuz  45765  limsupre2mpt  45768  limsupre3  45771  limsupre3mpt  45772  limsupre3uz  45774  limsupreuz  45775  limsupreuzmpt  45777  supcnvlimsup  45778  climuz  45782  lmbr3  45785  climrescn  45786  limsuplt2  45791  liminflelimsup  45814  limsupgt  45816  liminfreuz  45841  liminflt  45843  xlimpnfxnegmnf  45852  xlimmnf  45879  xlimpnf  45880  xlimmnfmpt  45881  xlimpnfmpt  45882  dfxlim2  45886  cncfshiftioo  45930  itgiccshift  46018  itgperiod  46019  fourierdlem42  46187  fourierdlem48  46192  fourierdlem81  46225  fourierdlem92  46236  fourierdlem96  46240  fourierdlem97  46241  fourierdlem98  46242  fourierdlem99  46243  fourierdlem105  46249  fourierdlem108  46252  fourierdlem110  46254  fourierdlem112  46256  fourierdlem113  46257  meaiunincf  46521  meaiuninc3v  46522  hoidmvval0  46625  ovnhoi  46641  ovolval5lem3  46692  ovolval5  46693  smfsup  46852  smfinflem  46855  smfinf  46856  fsetsnfo  47084  2reuimp0  47145  imaelsetpreimafv  47426  imasetpreimafvbijlemfo  47436  fundcmpsurinj  47440  fundcmpsurbijinj  47441  fmtnofac2lem  47599  2zlidl  48271  2zrngamgm  48276  2zrngagrp  48280  2zrngmmgm  48283  eenglngeehlnmlem1  48769  upciclem4  49201