Theorem cbvrexvw 3242

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 2178, ax-11 2194, ax-12 2213, 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 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2070	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3088	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3088	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-rex 3088

This theorem is used by:  cbvrex2vw  3246  reu7  3690  cbviunv  4997  disjiund  5094  reusv3  5367  xpdifid  6159  xpdifcnvepel  6160  fliftfun  7318  funcnvuni  7942  fiunlem  7952  poseq  8168  soseq  8169  nneob  8658  coflton  8673  cofon1  8674  cofon2  8675  pssnn  9177  frfi  9269  finsschain  9341  marypha1lem  9418  supmo  9437  suplub2  9446  infmo  9482  ordtypelem3  9507  ordtypelem9  9513  wemaplem1  9533  brwdom3  9569  unwdomg  9571  cantnf  9687  ttrcltr  9710  trcl  9722  infxpenc2  10094  aceq2  10191  dfac5lem4  10198  kmlem9  10230  kmlem14  10235  fin23lem26  10396  fin1a2lem13  10483  axdc3lem3  10523  winainflem  10771  axgroth4  10910  suprlub  12274  supaddc  12277  supadd  12278  supmul1  12279  supmullem1  12280  supmullem2  12281  supmul  12282  ublbneg  13053  zsupss  13057  xrsupsslem  13430  xrinfmsslem  13431  rexanre  15507  rexuzre  15513  rexico  15514  caurcvg2  15838  caucvgb  15840  summolem2  15875  summo  15876  mertens  16048  prodmolem2  16095  prodmo  16096  odd2np1lem  16503  gcdcllem1  16662  prmdvdsncoprmbd  16896  pceu  17017  4sqlem12  17127  vdwlem10  17161  vdwlem13  17164  vdwnn  17169  drsdirfi  18472  0gisid  18841  grprida  18849  smndex1mgm  19099  smndex1mndlem  19101  dfgrp2  19166  dfgrp3lem  19241  cyccom  19411  gaorb  19514  psgnunilem3  19703  psgnunilem4  19704  psgneu  19713  pj1eu  19903  efgsfo  19946  cyggeninv  20090  cygabl  20098  pgpfac1lem5  20288  pgpfac1  20289  pgpfaclem2  20291  isdrng4  20985  isdrng3lem2  20999  lss1d  21231  lspsneq  21393  lspsolvlem  21413  lbsextlem2  21430  cygznlem3  21868  mplcoe5lem  22341  pmatcollpw3fi1lem2  23098  ordtrest2lem  23514  cnprest  23600  1stcfb  23756  1stcelcls  23773  elpt  23884  fbssfi  24149  fgcl  24190  rnelfmlem  24264  fmfnfmlem3  24268  txflf  24318  alexsubb  24358  alexsubALTlem4  24362  isucn2  24590  icccmplem2  25136  ply1divex  26448  coeeu  26537  plydivex  26611  aannenlem2  26649  ulmcau  26715  ulmbdd  26718  dchrptlem2  27585  bposlem9  27612  2lgslem1b  27712  pntibndlem3  27912  pntlemi  27924  pntlemp  27930  pntleml  27931  pnt3  27932  nosupprefixmo  28050  noinfprefixmo  28051  nosupcbv  28052  nosupdm  28054  nosupfv  28056  nosupres  28057  nosupbnd1lem1  28058  nosupbnd1lem4  28061  noinfcbv  28067  noinfdm  28069  noinfbnd1lem4  28076  cofslts  28297  coinitslts  28298  addsval2  28342  addcuts  28357  addsunif  28381  norecdiv  28569  recsne0  28571  bdayn0sf1o  28749  dfnns2  28751  n0seo  28800  pw2recs  28817  bdayfinbndcbv  28845  bdayfinbndlem1  28846  bdayfinbndlem2  28847  recut  28873  readdscl  28878  legval  29040  legov  29041  legov2  29042  outpasch  29226  lnopp2hpgb  29234  colopp  29240  elplngid  29253  lnincplng  29255  plngcp  29257  plngrot  29261  nhpmirhp  29269  lnperpexs  29303  ragraghl  29339  tgaaddcpbllem2  29343  tgaaddcpbllem3  29344  tgaaddcpbl2  29346  angmgmaddeu1  29372  angmgmaddcl  29384  prlnghpg  29417  prlngmo  29425  tgaltai  29438  erclwwlksym  30605  erclwwlktr  30606  erclwwlknsym  30654  erclwwlkntr  30655  eleclclwwlkn  30660  hashecclwwlkn1  30661  umgrhashecclwwlk  30662  grpoidinvlem3  31101  ubthlem3  31467  norm1exi  31845  pjhthmo  31897  cdjreui  33027  cdj3i  33036  infxrge0glb  33350  mndlrinvb  33579  gsumwrd2dccatlem  33631  cyc3genpm  33706  isarchi3  33741  archiabl  33752  erler  33819  rlocisunit  33830  1arithidomlem1  34060  1arithidom  34062  1arithufdlem2  34070  1arithufdlem3  34071  1arithufd  34073  fldext2chn  34353  constrconj  34370  constrextdg2lem  34373  constrextdg2  34374  constrfiss  34376  zarclsun  34495  ordtrest2NEWlem  34547  lmxrge0  34577  esumcvg  34711  esum2d  34718  eulerpartlems  34985  eulerpartlemgvv  35001  onvf1odlem2  35866  connpconn  35979  cvmlift2lem12  36058  cvmlift2lem13  36059  cvmlift3lem2  36064  cvmlift3lem7  36069  cvmlift3  36072  fmlasuc  36130  fmla1  36131  satffunlem1lem1  36146  satffunlem2lem1  36148  r1peuqusdeg1  36387  funtransport  36776  funray  36885  funline  36887  fnessref  37125  neibastop2  37129  dissneqlem  38243  dissneq  38244  pibt2  38320  ptrest  38517  poimirlem27  38545  poimirlem32  38550  ismblfin  38559  volsupnfl  38563  itg2addnclem  38569  unirep  38628  filbcmb  38654  sdclem1  38657  sdc  38658  fdc  38659  incsequz  38662  heibor1lem  38723  heiborlem10  38734  isgrpda  38869  isdrngo2  38872  prnc  38981  prtlem13  39905  prtlem15  39912  lshpsmreu  40146  lshpkrlem1  40147  lshpkrlem3  40149  pclfinN  40937  4atex  41113  dihglblem2N  42331  lcfl7N  42538  lcf1o  42588  supinf  43273  fimgmcyclem  43577  mzpcompact2lem  43741  eldioph3  43756  diophrex  43765  rexrabdioph  43780  eldioph4i  43798  aomclem8  44047  hbtlem2  44110  rngunsnply  44155  onsucrn  44257  iunrelexpuztr  44704  ntrclsneine0lem  45049  rexlimddvcbvw  45189  cpcoll2d  45228  mnuprdlem3  45243  dvconstbi  45303  expgrowth  45304  wessf1ornlem  46169  rnmptlb  46224  rnmptbdd  46226  rnmptbd2  46230  rnmptbd  46237  rexabsle  46398  uzub  46410  infrpgernmpt  46444  limcperiod  46609  limsupre  46620  limsupbnd1f  46665  climinf2  46686  climinfmpt  46694  limsupubuzmpt  46698  limsupmnf  46700  limsupre2  46704  limsupmnfuzlem  46705  limsupmnfuz  46706  limsupre2mpt  46709  limsupre3  46712  limsupre3mpt  46713  limsupre3uz  46715  limsupreuz  46716  limsupreuzmpt  46718  supcnvlimsup  46719  climuz  46723  lmbr3  46726  climrescn  46727  limsuplt2  46732  liminflelimsup  46755  limsupgt  46757  liminfreuz  46782  liminflt  46784  xlimpnfxnegmnf  46793  xlimmnf  46820  xlimpnf  46821  xlimmnfmpt  46822  xlimpnfmpt  46823  dfxlim2  46827  cncfshiftioo  46871  itgiccshift  46959  itgperiod  46960  fourierdlem42  47128  fourierdlem48  47133  fourierdlem81  47166  fourierdlem92  47177  fourierdlem96  47181  fourierdlem97  47182  fourierdlem98  47183  fourierdlem99  47184  fourierdlem105  47190  fourierdlem108  47193  fourierdlem110  47195  fourierdlem112  47197  fourierdlem113  47198  meaiunincf  47462  meaiuninc3v  47463  hoidmvval0  47566  ovnhoi  47582  ovolval5lem3  47633  ovolval5  47634  smfsup  47793  smfinflem  47796  smfinf  47797  fsetsnfo  48092  2reuimp0  48153  nndivides2  48423  imaelsetpreimafv  48446  imasetpreimafvbijlemfo  48456  fundcmpsurinj  48460  fundcmpsurbijinj  48461  fmtnofac2lem  48622  2zlidl  49306  2zrngamgm  49311  2zrngagrp  49315  2zrngmmgm  49318  eenglngeehlnmlem1  49818  upciclem4  50246