Theorem cbvrexvw 3236

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3363 with a disjoint variable condition, which does not require ax-10 2139, ax-11 2155, ax-12 2175, ax-13 2375. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2375. (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 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2034	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3069	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∃wex 1776   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814  df-rex 3069

This theorem is referenced by:  cbvrex2vw  3240  reu7  3741  cbviunv  5045  disjiund  5139  reusv3  5411  xpdifid  6190  fliftfun  7332  funcnvuni  7955  fiunlem  7965  poseq  8182  soseq  8183  nneob  8693  coflton  8708  cofon1  8709  cofon2  8710  pssnn  9207  frfi  9319  finsschain  9397  marypha1lem  9471  supmo  9490  suplub2  9499  infmo  9533  ordtypelem3  9558  ordtypelem9  9564  wemaplem1  9584  brwdom3  9620  unwdomg  9622  cantnf  9731  ttrcltr  9754  trcl  9766  infxpenc2  10060  aceq2  10157  dfac5lem4  10164  dfac5lem4OLD  10166  kmlem9  10197  kmlem14  10202  fin23lem26  10363  fin1a2lem13  10450  axdc3lem3  10490  winainflem  10731  axgroth4  10870  suprlub  12230  supaddc  12233  supadd  12234  supmul1  12235  supmullem1  12236  supmullem2  12237  supmul  12238  ublbneg  12973  zsupss  12977  xrsupsslem  13346  xrinfmsslem  13347  rexanre  15382  rexuzre  15388  rexico  15389  caurcvg2  15711  caucvgb  15713  summolem2  15749  summo  15750  mertens  15919  prodmolem2  15968  prodmo  15969  odd2np1lem  16374  gcdcllem1  16533  prmdvdsncoprmbd  16761  pceu  16880  4sqlem12  16990  vdwlem10  17024  vdwlem13  17027  vdwnn  17032  drsdirfi  18363  grprida  18701  smndex1mgm  18933  smndex1mndlem  18935  dfgrp2  18993  dfgrp3lem  19069  cyccom  19234  gaorb  19338  psgnunilem3  19529  psgnunilem4  19530  psgneu  19539  pj1eu  19729  efgsfo  19772  cyggeninv  19916  cygabl  19924  pgpfac1lem5  20114  pgpfac1  20115  pgpfaclem2  20117  lss1d  20979  lspsneq  21142  lspsolvlem  21162  lbsextlem2  21179  cygznlem3  21606  mplcoe5lem  22075  pmatcollpw3fi1lem2  22809  ordtrest2lem  23227  cnprest  23313  1stcfb  23469  1stcelcls  23485  elpt  23596  fbssfi  23861  fgcl  23902  rnelfmlem  23976  fmfnfmlem3  23980  txflf  24030  alexsubb  24070  alexsubALTlem4  24074  isucn2  24304  icccmplem2  24859  ply1divex  26191  coeeu  26279  plydivex  26354  aannenlem2  26386  ulmcau  26453  ulmbdd  26456  dchrptlem2  27324  bposlem9  27351  2lgslem1b  27451  pntibndlem3  27651  pntlemi  27663  pntlemp  27669  pntleml  27670  pnt3  27671  nosupprefixmo  27760  noinfprefixmo  27761  nosupcbv  27762  nosupdm  27764  nosupfv  27766  nosupres  27767  nosupbnd1lem1  27768  nosupbnd1lem4  27771  noinfcbv  27777  noinfdm  27779  noinfbnd1lem4  27786  cofsslt  27967  coinitsslt  27968  addsval2  28011  addscut  28026  addsunif  28050  norecdiv  28231  dfnns2  28377  n0seo  28420  recut  28443  readdscl  28446  legval  28607  legov  28608  legov2  28609  outpasch  28778  lnopp2hpgb  28786  colopp  28792  erclwwlksym  30050  erclwwlktr  30051  erclwwlknsym  30099  erclwwlkntr  30100  eleclclwwlkn  30105  hashecclwwlkn1  30106  umgrhashecclwwlk  30107  grpoidinvlem3  30535  ubthlem3  30901  norm1exi  31279  pjhthmo  31331  cdjreui  32461  cdj3i  32470  infxrge0glb  32776  mndlrinvb  33013  gsumwrd2dccatlem  33052  cyc3genpm  33155  isarchi3  33177  archiabl  33188  erler  33252  isdrng4  33279  1arithidomlem1  33543  1arithidom  33545  1arithufdlem2  33553  1arithufdlem3  33554  1arithufd  33556  fldext2chn  33734  constrconj  33750  zarclsun  33831  ordtrest2NEWlem  33883  lmxrge0  33913  esumcvg  34067  esum2d  34074  eulerpartlems  34342  eulerpartlemgvv  34358  connpconn  35220  cvmlift2lem12  35299  cvmlift2lem13  35300  cvmlift3lem2  35305  cvmlift3lem7  35310  cvmlift3  35313  fmlasuc  35371  fmla1  35372  satffunlem1lem1  35387  satffunlem2lem1  35389  r1peuqusdeg1  35628  funtransport  36013  funray  36122  funline  36124  fnessref  36340  neibastop2  36344  dissneqlem  37323  dissneq  37324  pibt2  37400  ptrest  37606  poimirlem27  37634  poimirlem32  37639  ismblfin  37648  volsupnfl  37652  itg2addnclem  37658  unirep  37701  filbcmb  37727  sdclem1  37730  sdc  37731  fdc  37732  incsequz  37735  heibor1lem  37796  heiborlem10  37807  isgrpda  37942  isdrngo2  37945  prnc  38054  prtlem13  38850  prtlem15  38857  lshpsmreu  39091  lshpkrlem1  39092  lshpkrlem3  39094  pclfinN  39883  4atex  40059  dihglblem2N  41277  lcfl7N  41484  lcf1o  41534  supinf  42262  fimgmcyclem  42520  mzpcompact2lem  42739  eldioph3  42754  diophrex  42763  rexrabdioph  42782  eldioph4i  42800  aomclem8  43050  hbtlem2  43113  rngunsnply  43158  onsucrn  43261  iunrelexpuztr  43709  ntrclsneine0lem  44054  rexlimddvcbvw  44196  cpcoll2d  44255  mnuprdlem3  44270  dvconstbi  44330  expgrowth  44331  wessf1ornlem  45128  rnmptlb  45188  rnmptbdd  45190  rnmptbd2  45194  rnmptbd  45201  rexabsle  45369  uzub  45381  infrpgernmpt  45415  limcperiod  45584  limsupre  45597  limsupbnd1f  45642  climinf2  45663  climinfmpt  45671  limsupubuzmpt  45675  limsupmnf  45677  limsupre2  45681  limsupmnfuzlem  45682  limsupmnfuz  45683  limsupre2mpt  45686  limsupre3  45689  limsupre3mpt  45690  limsupre3uz  45692  limsupreuz  45693  limsupreuzmpt  45695  supcnvlimsup  45696  climuz  45700  lmbr3  45703  climrescn  45704  limsuplt2  45709  liminflelimsup  45732  limsupgt  45734  liminfreuz  45759  liminflt  45761  xlimpnfxnegmnf  45770  xlimmnf  45797  xlimpnf  45798  xlimmnfmpt  45799  xlimpnfmpt  45800  dfxlim2  45804  cncfshiftioo  45848  itgiccshift  45936  itgperiod  45937  fourierdlem42  46105  fourierdlem48  46110  fourierdlem81  46143  fourierdlem92  46154  fourierdlem96  46158  fourierdlem97  46159  fourierdlem98  46160  fourierdlem99  46161  fourierdlem105  46167  fourierdlem108  46170  fourierdlem110  46172  fourierdlem112  46174  fourierdlem113  46175  meaiunincf  46439  meaiuninc3v  46440  hoidmvval0  46543  ovnhoi  46559  ovolval5lem3  46610  ovolval5  46611  smfsup  46770  smfinflem  46773  smfinf  46774  fsetsnfo  47003  2reuimp0  47064  imaelsetpreimafv  47320  imasetpreimafvbijlemfo  47330  fundcmpsurinj  47334  fundcmpsurbijinj  47335  fmtnofac2lem  47493  2zlidl  48084  2zrngamgm  48089  2zrngagrp  48093  2zrngmmgm  48096  eenglngeehlnmlem1  48587  upciclem4  48815