Theorem cbvrexvw 3217

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3337 with a disjoint variable condition, which does not require ax-10 2147, ax-11 2163, ax-12 2185, ax-13 2377. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2377. (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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2039	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3063	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3063	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-rex 3063

This theorem is referenced by:  cbvrex2vw  3221  reu7  3692  cbviunv  4996  disjiund  5091  reusv3  5352  xpdifid  6134  fliftfun  7268  funcnvuni  7884  fiunlem  7896  poseq  8110  soseq  8111  nneob  8594  coflton  8609  cofon1  8610  cofon2  8611  pssnn  9105  frfi  9197  finsschain  9271  marypha1lem  9348  supmo  9367  suplub2  9376  infmo  9412  ordtypelem3  9437  ordtypelem9  9443  wemaplem1  9463  brwdom3  9499  unwdomg  9501  cantnf  9614  ttrcltr  9637  trcl  9649  infxpenc2  9944  aceq2  10041  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem9  10081  kmlem14  10086  fin23lem26  10247  fin1a2lem13  10334  axdc3lem3  10374  winainflem  10616  axgroth4  10755  suprlub  12118  supaddc  12121  supadd  12122  supmul1  12123  supmullem1  12124  supmullem2  12125  supmul  12126  ublbneg  12858  zsupss  12862  xrsupsslem  13234  xrinfmsslem  13235  rexanre  15282  rexuzre  15288  rexico  15289  caurcvg2  15613  caucvgb  15615  summolem2  15651  summo  15652  mertens  15821  prodmolem2  15870  prodmo  15871  odd2np1lem  16279  gcdcllem1  16438  prmdvdsncoprmbd  16666  pceu  16786  4sqlem12  16896  vdwlem10  16930  vdwlem13  16933  vdwnn  16938  drsdirfi  18240  grprida  18612  smndex1mgm  18844  smndex1mndlem  18846  dfgrp2  18904  dfgrp3lem  18980  cyccom  19144  gaorb  19248  psgnunilem3  19437  psgnunilem4  19438  psgneu  19447  pj1eu  19637  efgsfo  19680  cyggeninv  19824  cygabl  19832  pgpfac1lem5  20022  pgpfac1  20023  pgpfaclem2  20025  lss1d  20926  lspsneq  21089  lspsolvlem  21109  lbsextlem2  21126  cygznlem3  21536  mplcoe5lem  22006  pmatcollpw3fi1lem2  22743  ordtrest2lem  23159  cnprest  23245  1stcfb  23401  1stcelcls  23417  elpt  23528  fbssfi  23793  fgcl  23834  rnelfmlem  23908  fmfnfmlem3  23912  txflf  23962  alexsubb  24002  alexsubALTlem4  24006  isucn2  24234  icccmplem2  24780  ply1divex  26110  coeeu  26198  plydivex  26273  aannenlem2  26305  ulmcau  26372  ulmbdd  26375  dchrptlem2  27244  bposlem9  27271  2lgslem1b  27371  pntibndlem3  27571  pntlemi  27583  pntlemp  27589  pntleml  27590  pnt3  27591  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupdm  27684  nosupfv  27686  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem4  27691  noinfcbv  27697  noinfdm  27699  noinfbnd1lem4  27706  cofslts  27926  coinitslts  27927  addsval2  27971  addcuts  27986  addsunif  28010  norecdiv  28198  recsne0  28200  bdayn0sf1o  28378  dfnns2  28380  n0seo  28429  pw2recs  28446  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  recut  28502  readdscl  28507  legval  28668  legov  28669  legov2  28670  outpasch  28839  lnopp2hpgb  28847  colopp  28853  erclwwlksym  30108  erclwwlktr  30109  erclwwlknsym  30157  erclwwlkntr  30158  eleclclwwlkn  30163  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  grpoidinvlem3  30594  ubthlem3  30960  norm1exi  31338  pjhthmo  31390  cdjreui  32520  cdj3i  32529  infxrge0glb  32856  mndlrinvb  33118  gsumwrd2dccatlem  33171  cyc3genpm  33246  isarchi3  33281  archiabl  33292  erler  33359  isdrng4  33389  1arithidomlem1  33628  1arithidom  33630  1arithufdlem2  33638  1arithufdlem3  33639  1arithufd  33641  fldext2chn  33906  constrconj  33923  constrextdg2lem  33926  constrextdg2  33927  constrfiss  33929  zarclsun  34048  ordtrest2NEWlem  34100  lmxrge0  34130  esumcvg  34264  esum2d  34271  eulerpartlems  34538  eulerpartlemgvv  34554  onvf1odlem2  35320  connpconn  35451  cvmlift2lem12  35530  cvmlift2lem13  35531  cvmlift3lem2  35536  cvmlift3lem7  35541  cvmlift3  35544  fmlasuc  35602  fmla1  35603  satffunlem1lem1  35618  satffunlem2lem1  35620  r1peuqusdeg1  35859  funtransport  36247  funray  36356  funline  36358  fnessref  36573  neibastop2  36577  dissneqlem  37595  dissneq  37596  pibt2  37672  ptrest  37870  poimirlem27  37898  poimirlem32  37903  ismblfin  37912  volsupnfl  37916  itg2addnclem  37922  unirep  37965  filbcmb  37991  sdclem1  37994  sdc  37995  fdc  37996  incsequz  37999  heibor1lem  38060  heiborlem10  38071  isgrpda  38206  isdrngo2  38209  prnc  38318  prtlem13  39244  prtlem15  39251  lshpsmreu  39485  lshpkrlem1  39486  lshpkrlem3  39488  pclfinN  40276  4atex  40452  dihglblem2N  41670  lcfl7N  41877  lcf1o  41927  supinf  42612  fimgmcyclem  42903  mzpcompact2lem  43108  eldioph3  43123  diophrex  43132  rexrabdioph  43151  eldioph4i  43169  aomclem8  43418  hbtlem2  43481  rngunsnply  43526  onsucrn  43628  iunrelexpuztr  44075  ntrclsneine0lem  44420  rexlimddvcbvw  44562  cpcoll2d  44615  mnuprdlem3  44630  dvconstbi  44690  expgrowth  44691  wessf1ornlem  45544  rnmptlb  45601  rnmptbdd  45603  rnmptbd2  45607  rnmptbd  45614  rexabsle  45777  uzub  45789  infrpgernmpt  45823  limcperiod  45988  limsupre  45999  limsupbnd1f  46044  climinf2  46065  climinfmpt  46073  limsupubuzmpt  46077  limsupmnf  46079  limsupre2  46083  limsupmnfuzlem  46084  limsupmnfuz  46085  limsupre2mpt  46088  limsupre3  46091  limsupre3mpt  46092  limsupre3uz  46094  limsupreuz  46095  limsupreuzmpt  46097  supcnvlimsup  46098  climuz  46102  lmbr3  46105  climrescn  46106  limsuplt2  46111  liminflelimsup  46134  limsupgt  46136  liminfreuz  46161  liminflt  46163  xlimpnfxnegmnf  46172  xlimmnf  46199  xlimpnf  46200  xlimmnfmpt  46201  xlimpnfmpt  46202  dfxlim2  46206  cncfshiftioo  46250  itgiccshift  46338  itgperiod  46339  fourierdlem42  46507  fourierdlem48  46512  fourierdlem81  46545  fourierdlem92  46556  fourierdlem96  46560  fourierdlem97  46561  fourierdlem98  46562  fourierdlem99  46563  fourierdlem105  46569  fourierdlem108  46572  fourierdlem110  46574  fourierdlem112  46576  fourierdlem113  46577  meaiunincf  46841  meaiuninc3v  46842  hoidmvval0  46945  ovnhoi  46961  ovolval5lem3  47012  ovolval5  47013  smfsup  47172  smfinflem  47175  smfinf  47176  nthrucw  47244  fsetsnfo  47413  2reuimp0  47474  imaelsetpreimafv  47755  imasetpreimafvbijlemfo  47765  fundcmpsurinj  47769  fundcmpsurbijinj  47770  fmtnofac2lem  47928  2zlidl  48600  2zrngamgm  48605  2zrngagrp  48609  2zrngmmgm  48612  eenglngeehlnmlem1  49097  upciclem4  49528