Theorem cbvrexvw 3218

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3329 with a disjoint variable condition, which does not require ax-10 2152, ax-11 2168, ax-12 2189, ax-13 2380. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2380. (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 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 638	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2044	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3064	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3064	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 304	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814  df-rex 3064

This theorem is referenced by:  cbvrex2vw  3222  reu7  3673  cbviunv  4968  disjiund  5063  reusv3  5334  xpdifid  6119  fliftfun  7256  funcnvuni  7872  fiunlem  7884  poseq  8098  soseq  8099  nneob  8582  coflton  8597  cofon1  8598  cofon2  8599  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  9605  ttrcltr  9628  trcl  9640  infxpenc2  9935  aceq2  10032  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem9  10072  kmlem14  10077  fin23lem26  10238  fin1a2lem13  10325  axdc3lem3  10365  winainflem  10607  axgroth4  10746  suprlub  12111  supaddc  12114  supadd  12115  supmul1  12116  supmullem1  12117  supmullem2  12118  supmul  12119  ublbneg  12874  zsupss  12878  xrsupsslem  13250  xrinfmsslem  13251  rexanre  15300  rexuzre  15306  rexico  15307  caurcvg2  15631  caucvgb  15633  summolem2  15669  summo  15670  mertens  15842  prodmolem2  15891  prodmo  15892  odd2np1lem  16300  gcdcllem1  16459  prmdvdsncoprmbd  16688  pceu  16808  4sqlem12  16918  vdwlem10  16952  vdwlem13  16955  vdwnn  16960  drsdirfi  18262  grprida  18634  smndex1mgm  18869  smndex1mndlem  18871  dfgrp2  18929  dfgrp3lem  19005  cyccom  19169  gaorb  19273  psgnunilem3  19462  psgnunilem4  19463  psgneu  19472  pj1eu  19662  efgsfo  19705  cyggeninv  19849  cygabl  19857  pgpfac1lem5  20047  pgpfac1  20048  pgpfaclem2  20050  lss1d  20953  lspsneq  21115  lspsolvlem  21135  lbsextlem2  21152  cygznlem3  21544  mplcoe5lem  22015  pmatcollpw3fi1lem2  22770  ordtrest2lem  23186  cnprest  23272  1stcfb  23428  1stcelcls  23444  elpt  23555  fbssfi  23820  fgcl  23861  rnelfmlem  23935  fmfnfmlem3  23939  txflf  23989  alexsubb  24029  alexsubALTlem4  24033  isucn2  24261  icccmplem2  24807  ply1divex  26120  coeeu  26208  plydivex  26281  aannenlem2  26313  ulmcau  26378  ulmbdd  26381  dchrptlem2  27246  bposlem9  27273  2lgslem1b  27373  pntibndlem3  27573  pntlemi  27585  pntlemp  27591  pntleml  27592  pnt3  27593  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupdm  27686  nosupfv  27688  nosupres  27689  nosupbnd1lem1  27690  nosupbnd1lem4  27693  noinfcbv  27699  noinfdm  27701  noinfbnd1lem4  27708  cofslts  27928  coinitslts  27929  addsval2  27973  addcuts  27988  addsunif  28012  norecdiv  28200  recsne0  28202  bdayn0sf1o  28380  dfnns2  28382  n0seo  28431  pw2recs  28448  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  recut  28504  readdscl  28509  legval  28670  legov  28671  legov2  28672  outpasch  28841  lnopp2hpgb  28849  colopp  28855  erclwwlksym  30109  erclwwlktr  30110  erclwwlknsym  30158  erclwwlkntr  30159  eleclclwwlkn  30164  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  grpoidinvlem3  30595  ubthlem3  30961  norm1exi  31339  pjhthmo  31391  cdjreui  32521  cdj3i  32530  infxrge0glb  32857  mndlrinvb  33104  gsumwrd2dccatlem  33158  cyc3genpm  33233  isarchi3  33268  archiabl  33279  erler  33346  isdrng4  33379  1arithidomlem1  33618  1arithidom  33620  1arithufdlem2  33628  1arithufdlem3  33629  1arithufd  33631  fldext2chn  33912  constrconj  33929  constrextdg2lem  33932  constrextdg2  33933  constrfiss  33935  zarclsun  34054  ordtrest2NEWlem  34106  lmxrge0  34136  esumcvg  34270  esum2d  34277  eulerpartlems  34544  eulerpartlemgvv  34560  onvf1odlem2  35332  connpconn  35463  cvmlift2lem12  35542  cvmlift2lem13  35543  cvmlift3lem2  35548  cvmlift3lem7  35553  cvmlift3  35556  fmlasuc  35614  fmla1  35615  satffunlem1lem1  35630  satffunlem2lem1  35632  r1peuqusdeg1  35871  funtransport  36259  funray  36368  funline  36370  fnessref  36585  neibastop2  36589  dissneqlem  37702  dissneq  37703  pibt2  37779  ptrest  37986  poimirlem27  38014  poimirlem32  38019  ismblfin  38028  volsupnfl  38032  itg2addnclem  38038  unirep  38081  filbcmb  38107  sdclem1  38110  sdc  38111  fdc  38112  incsequz  38115  heibor1lem  38176  heiborlem10  38187  isgrpda  38322  isdrngo2  38325  prnc  38434  prtlem13  39360  prtlem15  39367  lshpsmreu  39601  lshpkrlem1  39602  lshpkrlem3  39604  pclfinN  40392  4atex  40568  dihglblem2N  41786  lcfl7N  41993  lcf1o  42043  supinf  42726  fimgmcyclem  43019  mzpcompact2lem  43200  eldioph3  43215  diophrex  43224  rexrabdioph  43239  eldioph4i  43257  aomclem8  43506  hbtlem2  43569  rngunsnply  43614  onsucrn  43716  iunrelexpuztr  44163  ntrclsneine0lem  44508  rexlimddvcbvw  44650  cpcoll2d  44703  mnuprdlem3  44718  dvconstbi  44778  expgrowth  44779  wessf1ornlem  45632  rnmptlb  45687  rnmptbdd  45689  rnmptbd2  45693  rnmptbd  45700  rexabsle  45862  uzub  45874  infrpgernmpt  45908  limcperiod  46073  limsupre  46084  limsupbnd1f  46129  climinf2  46150  climinfmpt  46158  limsupubuzmpt  46162  limsupmnf  46164  limsupre2  46168  limsupmnfuzlem  46169  limsupmnfuz  46170  limsupre2mpt  46173  limsupre3  46176  limsupre3mpt  46177  limsupre3uz  46179  limsupreuz  46180  limsupreuzmpt  46182  supcnvlimsup  46183  climuz  46187  lmbr3  46190  climrescn  46191  limsuplt2  46196  liminflelimsup  46219  limsupgt  46221  liminfreuz  46246  liminflt  46248  xlimpnfxnegmnf  46257  xlimmnf  46284  xlimpnf  46285  xlimmnfmpt  46286  xlimpnfmpt  46287  dfxlim2  46291  cncfshiftioo  46335  itgiccshift  46423  itgperiod  46424  fourierdlem42  46592  fourierdlem48  46597  fourierdlem81  46630  fourierdlem92  46641  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem105  46654  fourierdlem108  46657  fourierdlem110  46659  fourierdlem112  46661  fourierdlem113  46662  meaiunincf  46926  meaiuninc3v  46927  hoidmvval0  47030  ovnhoi  47046  ovolval5lem3  47097  ovolval5  47098  smfsup  47257  smfinflem  47260  smfinf  47261  nthrucw  47331  fsetsnfo  47516  2reuimp0  47577  nndivides2  47847  imaelsetpreimafv  47870  imasetpreimafvbijlemfo  47880  fundcmpsurinj  47884  fundcmpsurbijinj  47885  fmtnofac2lem  48046  2zlidl  48731  2zrngamgm  48736  2zrngagrp  48740  2zrngmmgm  48743  eenglngeehlnmlem1  49228  upciclem4  49659