Theorem cbvrexvw 3216

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

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

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 2811  df-rex 3062

This theorem is referenced by:  cbvrex2vw  3220  reu7  3678  cbviunv  4981  disjiund  5076  reusv3  5347  xpdifid  6132  fliftfun  7267  funcnvuni  7883  fiunlem  7895  poseq  8108  soseq  8109  nneob  8592  coflton  8607  cofon1  8608  cofon2  8609  pssnn  9103  frfi  9195  finsschain  9269  marypha1lem  9346  supmo  9365  suplub2  9374  infmo  9410  ordtypelem3  9435  ordtypelem9  9441  wemaplem1  9461  brwdom3  9497  unwdomg  9499  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  12120  supaddc  12123  supadd  12124  supmul1  12125  supmullem1  12126  supmullem2  12127  supmul  12128  ublbneg  12883  zsupss  12887  xrsupsslem  13259  xrinfmsslem  13260  rexanre  15309  rexuzre  15315  rexico  15316  caurcvg2  15640  caucvgb  15642  summolem2  15678  summo  15679  mertens  15851  prodmolem2  15900  prodmo  15901  odd2np1lem  16309  gcdcllem1  16468  prmdvdsncoprmbd  16697  pceu  16817  4sqlem12  16927  vdwlem10  16961  vdwlem13  16964  vdwnn  16969  drsdirfi  18271  grprida  18643  smndex1mgm  18878  smndex1mndlem  18880  dfgrp2  18938  dfgrp3lem  19014  cyccom  19178  gaorb  19282  psgnunilem3  19471  psgnunilem4  19472  psgneu  19481  pj1eu  19671  efgsfo  19714  cyggeninv  19858  cygabl  19866  pgpfac1lem5  20056  pgpfac1  20057  pgpfaclem2  20059  lss1d  20958  lspsneq  21120  lspsolvlem  21140  lbsextlem2  21157  cygznlem3  21549  mplcoe5lem  22017  pmatcollpw3fi1lem2  22752  ordtrest2lem  23168  cnprest  23254  1stcfb  23410  1stcelcls  23426  elpt  23537  fbssfi  23802  fgcl  23843  rnelfmlem  23917  fmfnfmlem3  23921  txflf  23971  alexsubb  24011  alexsubALTlem4  24015  isucn2  24243  icccmplem2  24789  ply1divex  26102  coeeu  26190  plydivex  26263  aannenlem2  26295  ulmcau  26360  ulmbdd  26363  dchrptlem2  27228  bposlem9  27255  2lgslem1b  27355  pntibndlem3  27555  pntlemi  27567  pntlemp  27573  pntleml  27574  pnt3  27575  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupdm  27668  nosupfv  27670  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem4  27675  noinfcbv  27681  noinfdm  27683  noinfbnd1lem4  27690  cofslts  27910  coinitslts  27911  addsval2  27955  addcuts  27970  addsunif  27994  norecdiv  28182  recsne0  28184  bdayn0sf1o  28362  dfnns2  28364  n0seo  28413  pw2recs  28430  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  recut  28486  readdscl  28491  legval  28652  legov  28653  legov2  28654  outpasch  28823  lnopp2hpgb  28831  colopp  28837  erclwwlksym  30091  erclwwlktr  30092  erclwwlknsym  30140  erclwwlkntr  30141  eleclclwwlkn  30146  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  grpoidinvlem3  30577  ubthlem3  30943  norm1exi  31321  pjhthmo  31373  cdjreui  32503  cdj3i  32512  infxrge0glb  32838  mndlrinvb  33085  gsumwrd2dccatlem  33138  cyc3genpm  33213  isarchi3  33248  archiabl  33259  erler  33326  isdrng4  33356  1arithidomlem1  33595  1arithidom  33597  1arithufdlem2  33605  1arithufdlem3  33606  1arithufd  33608  fldext2chn  33872  constrconj  33889  constrextdg2lem  33892  constrextdg2  33893  constrfiss  33895  zarclsun  34014  ordtrest2NEWlem  34066  lmxrge0  34096  esumcvg  34230  esum2d  34237  eulerpartlems  34504  eulerpartlemgvv  34520  onvf1odlem2  35286  connpconn  35417  cvmlift2lem12  35496  cvmlift2lem13  35497  cvmlift3lem2  35502  cvmlift3lem7  35507  cvmlift3  35510  fmlasuc  35568  fmla1  35569  satffunlem1lem1  35584  satffunlem2lem1  35586  r1peuqusdeg1  35825  funtransport  36213  funray  36322  funline  36324  fnessref  36539  neibastop2  36543  dissneqlem  37656  dissneq  37657  pibt2  37733  ptrest  37940  poimirlem27  37968  poimirlem32  37973  ismblfin  37982  volsupnfl  37986  itg2addnclem  37992  unirep  38035  filbcmb  38061  sdclem1  38064  sdc  38065  fdc  38066  incsequz  38069  heibor1lem  38130  heiborlem10  38141  isgrpda  38276  isdrngo2  38279  prnc  38388  prtlem13  39314  prtlem15  39321  lshpsmreu  39555  lshpkrlem1  39556  lshpkrlem3  39558  pclfinN  40346  4atex  40522  dihglblem2N  41740  lcfl7N  41947  lcf1o  41997  supinf  42681  fimgmcyclem  42978  mzpcompact2lem  43183  eldioph3  43198  diophrex  43207  rexrabdioph  43222  eldioph4i  43240  aomclem8  43489  hbtlem2  43552  rngunsnply  43597  onsucrn  43699  iunrelexpuztr  44146  ntrclsneine0lem  44491  rexlimddvcbvw  44633  cpcoll2d  44686  mnuprdlem3  44701  dvconstbi  44761  expgrowth  44762  wessf1ornlem  45615  rnmptlb  45672  rnmptbdd  45674  rnmptbd2  45678  rnmptbd  45685  rexabsle  45847  uzub  45859  infrpgernmpt  45893  limcperiod  46058  limsupre  46069  limsupbnd1f  46114  climinf2  46135  climinfmpt  46143  limsupubuzmpt  46147  limsupmnf  46149  limsupre2  46153  limsupmnfuzlem  46154  limsupmnfuz  46155  limsupre2mpt  46158  limsupre3  46161  limsupre3mpt  46162  limsupre3uz  46164  limsupreuz  46165  limsupreuzmpt  46167  supcnvlimsup  46168  climuz  46172  lmbr3  46175  climrescn  46176  limsuplt2  46181  liminflelimsup  46204  limsupgt  46206  liminfreuz  46231  liminflt  46233  xlimpnfxnegmnf  46242  xlimmnf  46269  xlimpnf  46270  xlimmnfmpt  46271  xlimpnfmpt  46272  dfxlim2  46276  cncfshiftioo  46320  itgiccshift  46408  itgperiod  46409  fourierdlem42  46577  fourierdlem48  46582  fourierdlem81  46615  fourierdlem92  46626  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem105  46639  fourierdlem108  46642  fourierdlem110  46644  fourierdlem112  46646  fourierdlem113  46647  meaiunincf  46911  meaiuninc3v  46912  hoidmvval0  47015  ovnhoi  47031  ovolval5lem3  47082  ovolval5  47083  smfsup  47242  smfinflem  47245  smfinf  47246  nthrucw  47316  fsetsnfo  47501  2reuimp0  47562  nndivides2  47832  imaelsetpreimafv  47855  imasetpreimafvbijlemfo  47865  fundcmpsurinj  47869  fundcmpsurbijinj  47870  fmtnofac2lem  48031  2zlidl  48716  2zrngamgm  48721  2zrngagrp  48725  2zrngmmgm  48728  eenglngeehlnmlem1  49213  upciclem4  49644