Theorem cbvrexvw 3215

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

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

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 2115

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

This theorem is referenced by:  cbvrex2vw  3219  reu7  3690  cbviunv  4994  disjiund  5089  reusv3  5350  xpdifid  6126  fliftfun  7258  funcnvuni  7874  fiunlem  7886  poseq  8100  soseq  8101  nneob  8584  coflton  8599  cofon1  8600  cofon2  8601  pssnn  9093  frfi  9185  finsschain  9259  marypha1lem  9336  supmo  9355  suplub2  9364  infmo  9400  ordtypelem3  9425  ordtypelem9  9431  wemaplem1  9451  brwdom3  9487  unwdomg  9489  cantnf  9602  ttrcltr  9625  trcl  9637  infxpenc2  9932  aceq2  10029  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem9  10069  kmlem14  10074  fin23lem26  10235  fin1a2lem13  10322  axdc3lem3  10362  winainflem  10604  axgroth4  10743  suprlub  12106  supaddc  12109  supadd  12110  supmul1  12111  supmullem1  12112  supmullem2  12113  supmul  12114  ublbneg  12846  zsupss  12850  xrsupsslem  13222  xrinfmsslem  13223  rexanre  15270  rexuzre  15276  rexico  15277  caurcvg2  15601  caucvgb  15603  summolem2  15639  summo  15640  mertens  15809  prodmolem2  15858  prodmo  15859  odd2np1lem  16267  gcdcllem1  16426  prmdvdsncoprmbd  16654  pceu  16774  4sqlem12  16884  vdwlem10  16918  vdwlem13  16921  vdwnn  16926  drsdirfi  18228  grprida  18600  smndex1mgm  18832  smndex1mndlem  18834  dfgrp2  18892  dfgrp3lem  18968  cyccom  19132  gaorb  19236  psgnunilem3  19425  psgnunilem4  19426  psgneu  19435  pj1eu  19625  efgsfo  19668  cyggeninv  19812  cygabl  19820  pgpfac1lem5  20010  pgpfac1  20011  pgpfaclem2  20013  lss1d  20914  lspsneq  21077  lspsolvlem  21097  lbsextlem2  21114  cygznlem3  21524  mplcoe5lem  21994  pmatcollpw3fi1lem2  22731  ordtrest2lem  23147  cnprest  23233  1stcfb  23389  1stcelcls  23405  elpt  23516  fbssfi  23781  fgcl  23822  rnelfmlem  23896  fmfnfmlem3  23900  txflf  23950  alexsubb  23990  alexsubALTlem4  23994  isucn2  24222  icccmplem2  24768  ply1divex  26098  coeeu  26186  plydivex  26261  aannenlem2  26293  ulmcau  26360  ulmbdd  26363  dchrptlem2  27232  bposlem9  27259  2lgslem1b  27359  pntibndlem3  27559  pntlemi  27571  pntlemp  27577  pntleml  27578  pnt3  27579  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupdm  27672  nosupfv  27674  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem4  27679  noinfcbv  27685  noinfdm  27687  noinfbnd1lem4  27694  cofslts  27914  coinitslts  27915  addsval2  27959  addcuts  27974  addsunif  27998  norecdiv  28186  recsne0  28188  bdayn0sf1o  28366  dfnns2  28368  n0seo  28417  pw2recs  28434  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  recut  28490  readdscl  28495  legval  28656  legov  28657  legov2  28658  outpasch  28827  lnopp2hpgb  28835  colopp  28841  erclwwlksym  30096  erclwwlktr  30097  erclwwlknsym  30145  erclwwlkntr  30146  eleclclwwlkn  30151  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  grpoidinvlem3  30581  ubthlem3  30947  norm1exi  31325  pjhthmo  31377  cdjreui  32507  cdj3i  32516  infxrge0glb  32845  mndlrinvb  33107  gsumwrd2dccatlem  33159  cyc3genpm  33234  isarchi3  33269  archiabl  33280  erler  33347  isdrng4  33377  1arithidomlem1  33616  1arithidom  33618  1arithufdlem2  33626  1arithufdlem3  33627  1arithufd  33629  fldext2chn  33885  constrconj  33902  constrextdg2lem  33905  constrextdg2  33906  constrfiss  33908  zarclsun  34027  ordtrest2NEWlem  34079  lmxrge0  34109  esumcvg  34243  esum2d  34250  eulerpartlems  34517  eulerpartlemgvv  34533  onvf1odlem2  35298  connpconn  35429  cvmlift2lem12  35508  cvmlift2lem13  35509  cvmlift3lem2  35514  cvmlift3lem7  35519  cvmlift3  35522  fmlasuc  35580  fmla1  35581  satffunlem1lem1  35596  satffunlem2lem1  35598  r1peuqusdeg1  35837  funtransport  36225  funray  36334  funline  36336  fnessref  36551  neibastop2  36555  dissneqlem  37545  dissneq  37546  pibt2  37622  ptrest  37820  poimirlem27  37848  poimirlem32  37853  ismblfin  37862  volsupnfl  37866  itg2addnclem  37872  unirep  37915  filbcmb  37941  sdclem1  37944  sdc  37945  fdc  37946  incsequz  37949  heibor1lem  38010  heiborlem10  38021  isgrpda  38156  isdrngo2  38159  prnc  38268  prtlem13  39128  prtlem15  39135  lshpsmreu  39369  lshpkrlem1  39370  lshpkrlem3  39372  pclfinN  40160  4atex  40336  dihglblem2N  41554  lcfl7N  41761  lcf1o  41811  supinf  42497  fimgmcyclem  42788  mzpcompact2lem  42993  eldioph3  43008  diophrex  43017  rexrabdioph  43036  eldioph4i  43054  aomclem8  43303  hbtlem2  43366  rngunsnply  43411  onsucrn  43513  iunrelexpuztr  43960  ntrclsneine0lem  44305  rexlimddvcbvw  44447  cpcoll2d  44500  mnuprdlem3  44515  dvconstbi  44575  expgrowth  44576  wessf1ornlem  45429  rnmptlb  45487  rnmptbdd  45489  rnmptbd2  45493  rnmptbd  45500  rexabsle  45663  uzub  45675  infrpgernmpt  45709  limcperiod  45874  limsupre  45885  limsupbnd1f  45930  climinf2  45951  climinfmpt  45959  limsupubuzmpt  45963  limsupmnf  45965  limsupre2  45969  limsupmnfuzlem  45970  limsupmnfuz  45971  limsupre2mpt  45974  limsupre3  45977  limsupre3mpt  45978  limsupre3uz  45980  limsupreuz  45981  limsupreuzmpt  45983  supcnvlimsup  45984  climuz  45988  lmbr3  45991  climrescn  45992  limsuplt2  45997  liminflelimsup  46020  limsupgt  46022  liminfreuz  46047  liminflt  46049  xlimpnfxnegmnf  46058  xlimmnf  46085  xlimpnf  46086  xlimmnfmpt  46087  xlimpnfmpt  46088  dfxlim2  46092  cncfshiftioo  46136  itgiccshift  46224  itgperiod  46225  fourierdlem42  46393  fourierdlem48  46398  fourierdlem81  46431  fourierdlem92  46442  fourierdlem96  46446  fourierdlem97  46447  fourierdlem98  46448  fourierdlem99  46449  fourierdlem105  46455  fourierdlem108  46458  fourierdlem110  46460  fourierdlem112  46462  fourierdlem113  46463  meaiunincf  46727  meaiuninc3v  46728  hoidmvval0  46831  ovnhoi  46847  ovolval5lem3  46898  ovolval5  46899  smfsup  47058  smfinflem  47061  smfinf  47062  nthrucw  47130  fsetsnfo  47299  2reuimp0  47360  imaelsetpreimafv  47641  imasetpreimafvbijlemfo  47651  fundcmpsurinj  47655  fundcmpsurbijinj  47656  fmtnofac2lem  47814  2zlidl  48486  2zrngamgm  48491  2zrngagrp  48495  2zrngmmgm  48498  eenglngeehlnmlem1  48983  upciclem4  49414