Theorem cbvrexvw 3221

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3344 with a disjoint variable condition, which does not require ax-10 2141, ax-11 2157, ax-12 2177, 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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2036	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3061	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3061	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2809  df-rex 3061

This theorem is referenced by:  cbvrex2vw  3225  reu7  3715  cbviunv  5016  disjiund  5110  reusv3  5375  xpdifid  6157  fliftfun  7305  funcnvuni  7928  fiunlem  7940  poseq  8157  soseq  8158  nneob  8668  coflton  8683  cofon1  8684  cofon2  8685  pssnn  9182  frfi  9293  finsschain  9371  marypha1lem  9445  supmo  9464  suplub2  9473  infmo  9509  ordtypelem3  9534  ordtypelem9  9540  wemaplem1  9560  brwdom3  9596  unwdomg  9598  cantnf  9707  ttrcltr  9730  trcl  9742  infxpenc2  10036  aceq2  10133  dfac5lem4  10140  dfac5lem4OLD  10142  kmlem9  10173  kmlem14  10178  fin23lem26  10339  fin1a2lem13  10426  axdc3lem3  10466  winainflem  10707  axgroth4  10846  suprlub  12206  supaddc  12209  supadd  12210  supmul1  12211  supmullem1  12212  supmullem2  12213  supmul  12214  ublbneg  12949  zsupss  12953  xrsupsslem  13323  xrinfmsslem  13324  rexanre  15365  rexuzre  15371  rexico  15372  caurcvg2  15694  caucvgb  15696  summolem2  15732  summo  15733  mertens  15902  prodmolem2  15951  prodmo  15952  odd2np1lem  16359  gcdcllem1  16518  prmdvdsncoprmbd  16746  pceu  16866  4sqlem12  16976  vdwlem10  17010  vdwlem13  17013  vdwnn  17018  drsdirfi  18317  grprida  18653  smndex1mgm  18885  smndex1mndlem  18887  dfgrp2  18945  dfgrp3lem  19021  cyccom  19186  gaorb  19290  psgnunilem3  19477  psgnunilem4  19478  psgneu  19487  pj1eu  19677  efgsfo  19720  cyggeninv  19864  cygabl  19872  pgpfac1lem5  20062  pgpfac1  20063  pgpfaclem2  20065  lss1d  20920  lspsneq  21083  lspsolvlem  21103  lbsextlem2  21120  cygznlem3  21530  mplcoe5lem  21997  pmatcollpw3fi1lem2  22725  ordtrest2lem  23141  cnprest  23227  1stcfb  23383  1stcelcls  23399  elpt  23510  fbssfi  23775  fgcl  23816  rnelfmlem  23890  fmfnfmlem3  23894  txflf  23944  alexsubb  23984  alexsubALTlem4  23988  isucn2  24217  icccmplem2  24763  ply1divex  26094  coeeu  26182  plydivex  26257  aannenlem2  26289  ulmcau  26356  ulmbdd  26359  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  cofsslt  27878  coinitsslt  27879  addsval2  27922  addscut  27937  addsunif  27961  norecdiv  28145  recsne0  28147  bdayn0sf1o  28311  dfnns2  28313  n0seo  28359  pw2recs  28375  recut  28399  readdscl  28402  legval  28563  legov  28564  legov2  28565  outpasch  28734  lnopp2hpgb  28742  colopp  28748  erclwwlksym  30002  erclwwlktr  30003  erclwwlknsym  30051  erclwwlkntr  30052  eleclclwwlkn  30057  hashecclwwlkn1  30058  umgrhashecclwwlk  30059  grpoidinvlem3  30487  ubthlem3  30853  norm1exi  31231  pjhthmo  31283  cdjreui  32413  cdj3i  32422  infxrge0glb  32742  mndlrinvb  33020  gsumwrd2dccatlem  33060  cyc3genpm  33163  isarchi3  33185  archiabl  33196  erler  33260  isdrng4  33289  1arithidomlem1  33550  1arithidom  33552  1arithufdlem2  33560  1arithufdlem3  33561  1arithufd  33563  fldext2chn  33762  constrconj  33779  constrextdg2lem  33782  constrextdg2  33783  constrfiss  33785  zarclsun  33901  ordtrest2NEWlem  33953  lmxrge0  33983  esumcvg  34117  esum2d  34124  eulerpartlems  34392  eulerpartlemgvv  34408  connpconn  35257  cvmlift2lem12  35336  cvmlift2lem13  35337  cvmlift3lem2  35342  cvmlift3lem7  35347  cvmlift3  35350  fmlasuc  35408  fmla1  35409  satffunlem1lem1  35424  satffunlem2lem1  35426  r1peuqusdeg1  35665  funtransport  36049  funray  36158  funline  36160  fnessref  36375  neibastop2  36379  dissneqlem  37358  dissneq  37359  pibt2  37435  ptrest  37643  poimirlem27  37671  poimirlem32  37676  ismblfin  37685  volsupnfl  37689  itg2addnclem  37695  unirep  37738  filbcmb  37764  sdclem1  37767  sdc  37768  fdc  37769  incsequz  37772  heibor1lem  37833  heiborlem10  37844  isgrpda  37979  isdrngo2  37982  prnc  38091  prtlem13  38886  prtlem15  38893  lshpsmreu  39127  lshpkrlem1  39128  lshpkrlem3  39130  pclfinN  39919  4atex  40095  dihglblem2N  41313  lcfl7N  41520  lcf1o  41570  supinf  42293  fimgmcyclem  42556  mzpcompact2lem  42774  eldioph3  42789  diophrex  42798  rexrabdioph  42817  eldioph4i  42835  aomclem8  43085  hbtlem2  43148  rngunsnply  43193  onsucrn  43295  iunrelexpuztr  43743  ntrclsneine0lem  44088  rexlimddvcbvw  44230  cpcoll2d  44283  mnuprdlem3  44298  dvconstbi  44358  expgrowth  44359  wessf1ornlem  45209  rnmptlb  45267  rnmptbdd  45269  rnmptbd2  45273  rnmptbd  45280  rexabsle  45446  uzub  45458  infrpgernmpt  45492  limcperiod  45657  limsupre  45670  limsupbnd1f  45715  climinf2  45736  climinfmpt  45744  limsupubuzmpt  45748  limsupmnf  45750  limsupre2  45754  limsupmnfuzlem  45755  limsupmnfuz  45756  limsupre2mpt  45759  limsupre3  45762  limsupre3mpt  45763  limsupre3uz  45765  limsupreuz  45766  limsupreuzmpt  45768  supcnvlimsup  45769  climuz  45773  lmbr3  45776  climrescn  45777  limsuplt2  45782  liminflelimsup  45805  limsupgt  45807  liminfreuz  45832  liminflt  45834  xlimpnfxnegmnf  45843  xlimmnf  45870  xlimpnf  45871  xlimmnfmpt  45872  xlimpnfmpt  45873  dfxlim2  45877  cncfshiftioo  45921  itgiccshift  46009  itgperiod  46010  fourierdlem42  46178  fourierdlem48  46183  fourierdlem81  46216  fourierdlem92  46227  fourierdlem96  46231  fourierdlem97  46232  fourierdlem98  46233  fourierdlem99  46234  fourierdlem105  46240  fourierdlem108  46243  fourierdlem110  46245  fourierdlem112  46247  fourierdlem113  46248  meaiunincf  46512  meaiuninc3v  46513  hoidmvval0  46616  ovnhoi  46632  ovolval5lem3  46683  ovolval5  46684  smfsup  46843  smfinflem  46846  smfinf  46847  fsetsnfo  47082  2reuimp0  47143  imaelsetpreimafv  47409  imasetpreimafvbijlemfo  47419  fundcmpsurinj  47423  fundcmpsurbijinj  47424  fmtnofac2lem  47582  2zlidl  48215  2zrngamgm  48220  2zrngagrp  48224  2zrngmmgm  48227  eenglngeehlnmlem1  48717  upciclem4  49104