Theorem cbvrexvw 3240

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3351 with a disjoint variable condition, which does not require ax-10 2174, ax-11 2190, ax-12 2211, ax-13 2402. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2402. (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 2844	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 641	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2056	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3086	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3086	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 305	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-rex 3086

This theorem is referenced by:  cbvrex2vw  3244  reu7  3693  cbviunv  4993  disjiund  5088  reusv3  5359  xpdifid  6149  fliftfun  7291  funcnvuni  7908  fiunlem  7918  poseq  8132  soseq  8133  nneob  8620  coflton  8635  cofon1  8636  cofon2  8637  pssnn  9131  frfi  9223  finsschain  9296  marypha1lem  9373  supmo  9392  suplub2  9401  infmo  9437  ordtypelem3  9462  ordtypelem9  9468  wemaplem1  9488  brwdom3  9524  unwdomg  9526  cantnf  9642  ttrcltr  9665  trcl  9677  infxpenc2  9972  aceq2  10069  dfac5lem4  10076  dfac5lem4OLD  10078  kmlem9  10109  kmlem14  10114  fin23lem26  10276  fin1a2lem13  10363  axdc3lem3  10403  winainflem  10645  axgroth4  10784  suprlub  12150  supaddc  12153  supadd  12154  supmul1  12155  supmullem1  12156  supmullem2  12157  supmul  12158  ublbneg  12928  zsupss  12932  xrsupsslem  13304  xrinfmsslem  13305  rexanre  15365  rexuzre  15371  rexico  15372  caurcvg2  15696  caucvgb  15698  summolem2  15734  summo  15735  mertens  15907  prodmolem2  15956  prodmo  15957  odd2np1lem  16365  gcdcllem1  16524  prmdvdsncoprmbd  16753  pceu  16873  4sqlem12  16983  vdwlem10  17017  vdwlem13  17020  vdwnn  17025  drsdirfi  18328  grprida  18700  smndex1mgm  18935  smndex1mndlem  18937  dfgrp2  18995  dfgrp3lem  19071  cyccom  19235  gaorb  19338  psgnunilem3  19527  psgnunilem4  19528  psgneu  19537  pj1eu  19727  efgsfo  19770  cyggeninv  19914  cygabl  19922  pgpfac1lem5  20112  pgpfac1  20113  pgpfaclem2  20115  lss1d  21018  lspsneq  21180  lspsolvlem  21200  lbsextlem2  21217  cygznlem3  21609  mplcoe5lem  22080  pmatcollpw3fi1lem2  22835  ordtrest2lem  23251  cnprest  23337  1stcfb  23493  1stcelcls  23509  elpt  23620  fbssfi  23885  fgcl  23926  rnelfmlem  24000  fmfnfmlem3  24004  txflf  24054  alexsubb  24094  alexsubALTlem4  24098  isucn2  24326  icccmplem2  24872  ply1divex  26185  coeeu  26273  plydivex  26349  aannenlem2  26381  ulmcau  26446  ulmbdd  26449  dchrptlem2  27317  bposlem9  27344  2lgslem1b  27444  pntibndlem3  27644  pntlemi  27656  pntlemp  27662  pntleml  27663  pnt3  27664  nosupprefixmo  27752  noinfprefixmo  27753  nosupcbv  27754  nosupdm  27756  nosupfv  27758  nosupres  27759  nosupbnd1lem1  27760  nosupbnd1lem4  27763  noinfcbv  27769  noinfdm  27771  noinfbnd1lem4  27778  cofslts  27999  coinitslts  28000  addsval2  28044  addcuts  28059  addsunif  28083  norecdiv  28271  recsne0  28273  bdayn0sf1o  28451  dfnns2  28453  n0seo  28502  pw2recs  28519  bdayfinbndcbv  28547  bdayfinbndlem1  28548  bdayfinbndlem2  28549  recut  28575  readdscl  28580  legval  28741  legov  28742  legov2  28743  outpasch  28912  lnopp2hpgb  28920  colopp  28926  erclwwlksym  30180  erclwwlktr  30181  erclwwlknsym  30229  erclwwlkntr  30230  eleclclwwlkn  30235  hashecclwwlkn1  30236  umgrhashecclwwlk  30237  grpoidinvlem3  30666  ubthlem3  31032  norm1exi  31410  pjhthmo  31462  cdjreui  32592  cdj3i  32601  infxrge0glb  32928  mndlrinvb  33164  gsumwrd2dccatlem  33218  cyc3genpm  33293  isarchi3  33328  archiabl  33339  erler  33407  rlocisunit  33418  isdrng4  33443  1arithidomlem1  33692  1arithidom  33694  1arithufdlem2  33702  1arithufdlem3  33703  1arithufd  33705  fldext2chn  33986  constrconj  34003  constrextdg2lem  34006  constrextdg2  34007  constrfiss  34009  zarclsun  34128  ordtrest2NEWlem  34180  lmxrge0  34210  esumcvg  34344  esum2d  34351  eulerpartlems  34618  eulerpartlemgvv  34634  onvf1odlem2  35408  connpconn  35546  cvmlift2lem12  35625  cvmlift2lem13  35626  cvmlift3lem2  35631  cvmlift3lem7  35636  cvmlift3  35639  fmlasuc  35697  fmla1  35698  satffunlem1lem1  35713  satffunlem2lem1  35715  r1peuqusdeg1  35954  funtransport  36342  funray  36451  funline  36453  fnessref  36678  neibastop2  36682  dissneqlem  37795  dissneq  37796  pibt2  37872  ptrest  38079  poimirlem27  38107  poimirlem32  38112  ismblfin  38121  volsupnfl  38125  itg2addnclem  38131  unirep  38174  filbcmb  38200  sdclem1  38203  sdc  38204  fdc  38205  incsequz  38208  heibor1lem  38269  heiborlem10  38280  isgrpda  38415  isdrngo2  38418  prnc  38527  prtlem13  39453  prtlem15  39460  lshpsmreu  39694  lshpkrlem1  39695  lshpkrlem3  39697  pclfinN  40485  4atex  40661  dihglblem2N  41879  lcfl7N  42086  lcf1o  42136  supinf  42819  fimgmcyclem  43112  mzpcompact2lem  43293  eldioph3  43308  diophrex  43317  rexrabdioph  43332  eldioph4i  43350  aomclem8  43599  hbtlem2  43662  rngunsnply  43707  onsucrn  43809  iunrelexpuztr  44256  ntrclsneine0lem  44601  rexlimddvcbvw  44743  cpcoll2d  44796  mnuprdlem3  44811  dvconstbi  44871  expgrowth  44872  wessf1ornlem  45724  rnmptlb  45779  rnmptbdd  45781  rnmptbd2  45785  rnmptbd  45792  rexabsle  45954  uzub  45966  infrpgernmpt  46000  limcperiod  46165  limsupre  46176  limsupbnd1f  46221  climinf2  46242  climinfmpt  46250  limsupubuzmpt  46254  limsupmnf  46256  limsupre2  46260  limsupmnfuzlem  46261  limsupmnfuz  46262  limsupre2mpt  46265  limsupre3  46268  limsupre3mpt  46269  limsupre3uz  46271  limsupreuz  46272  limsupreuzmpt  46274  supcnvlimsup  46275  climuz  46279  lmbr3  46282  climrescn  46283  limsuplt2  46288  liminflelimsup  46311  limsupgt  46313  liminfreuz  46338  liminflt  46340  xlimpnfxnegmnf  46349  xlimmnf  46376  xlimpnf  46377  xlimmnfmpt  46378  xlimpnfmpt  46379  dfxlim2  46383  cncfshiftioo  46427  itgiccshift  46515  itgperiod  46516  fourierdlem42  46684  fourierdlem48  46689  fourierdlem81  46722  fourierdlem92  46733  fourierdlem96  46737  fourierdlem97  46738  fourierdlem98  46739  fourierdlem99  46740  fourierdlem105  46746  fourierdlem108  46749  fourierdlem110  46751  fourierdlem112  46753  fourierdlem113  46754  meaiunincf  47018  meaiuninc3v  47019  hoidmvval0  47122  ovnhoi  47138  ovolval5lem3  47189  ovolval5  47190  smfsup  47349  smfinflem  47352  smfinf  47353  nthrucw  47423  fsetsnfo  47608  2reuimp0  47669  nndivides2  47939  imaelsetpreimafv  47962  imasetpreimafvbijlemfo  47972  fundcmpsurinj  47976  fundcmpsurbijinj  47977  fmtnofac2lem  48138  2zlidl  48823  2zrngamgm  48828  2zrngagrp  48832  2zrngmmgm  48835  eenglngeehlnmlem1  49320  upciclem4  49751