Theorem cbvrexvw 3241

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv 3350 with a disjoint variable condition, which does not require ax-10 2177, ax-11 2193, ax-12 2212, ax-13 2401. (Contributed by NM, 2-Jun-1998.) Avoid ax-13 2401. (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 2843	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvexvw 2069	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
5		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3087	. 2 ⊢ (∃𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-rex 3087

This theorem is used by:  cbvrex2vw  3245  reu7  3689  cbviunv  4996  disjiund  5093  reusv3  5366  xpdifid  6158  xpdifcnvepel  6159  fliftfun  7320  funcnvuni  7944  fiunlem  7954  poseq  8175  soseq  8176  nneob  8665  coflton  8680  cofon1  8681  cofon2  8682  pssnn  9184  frfi  9276  finsschain  9348  marypha1lem  9425  supmo  9444  suplub2  9453  infmo  9489  ordtypelem3  9514  ordtypelem9  9520  wemaplem1  9540  brwdom3  9576  unwdomg  9578  cantnf  9694  ttrcltr  9717  trcl  9729  infxpenc2  10101  aceq2  10198  dfac5lem4  10205  kmlem9  10237  kmlem14  10242  fin23lem26  10403  fin1a2lem13  10490  axdc3lem3  10530  winainflem  10778  axgroth4  10917  suprlub  12281  supaddc  12284  supadd  12285  supmul1  12286  supmullem1  12287  supmullem2  12288  supmul  12289  ublbneg  13060  zsupss  13064  xrsupsslem  13437  xrinfmsslem  13438  rexanre  15514  rexuzre  15520  rexico  15521  caurcvg2  15845  caucvgb  15847  summolem2  15882  summo  15883  mertens  16055  prodmolem2  16102  prodmo  16103  odd2np1lem  16510  gcdcllem1  16669  prmdvdsncoprmbd  16903  pceu  17024  4sqlem12  17134  vdwlem10  17168  vdwlem13  17171  vdwnn  17176  drsdirfi  18479  0gisid  18848  grprida  18856  smndex1mgm  19106  smndex1mndlem  19108  dfgrp2  19173  dfgrp3lem  19248  cyccom  19418  gaorb  19521  psgnunilem3  19710  psgnunilem4  19711  psgneu  19720  pj1eu  19910  efgsfo  19953  cyggeninv  20097  cygabl  20105  pgpfac1lem5  20295  pgpfac1  20296  pgpfaclem2  20298  isdrng4  20992  isdrng3lem2  21006  lss1d  21238  lspsneq  21400  lspsolvlem  21420  lbsextlem2  21437  cygznlem3  21875  mplcoe5lem  22348  pmatcollpw3fi1lem2  23105  ordtrest2lem  23521  cnprest  23607  1stcfb  23763  1stcelcls  23780  elpt  23891  fbssfi  24156  fgcl  24197  rnelfmlem  24271  fmfnfmlem3  24275  txflf  24325  alexsubb  24365  alexsubALTlem4  24369  isucn2  24597  icccmplem2  25143  ply1divex  26455  coeeu  26544  plydivex  26618  aannenlem2  26656  ulmcau  26722  ulmbdd  26725  dchrptlem2  27592  bposlem9  27619  2lgslem1b  27719  pntibndlem3  27919  pntlemi  27931  pntlemp  27937  pntleml  27938  pnt3  27939  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupdm  28061  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem4  28068  noinfcbv  28074  noinfdm  28076  noinfbnd1lem4  28083  cofslts  28304  coinitslts  28305  addsval2  28349  addcuts  28364  addsunif  28388  norecdiv  28576  recsne0  28578  bdayn0sf1o  28756  dfnns2  28758  n0seo  28807  pw2recs  28824  bdayfinbndcbv  28852  bdayfinbndlem1  28853  bdayfinbndlem2  28854  recut  28880  readdscl  28885  legval  29047  legov  29048  legov2  29049  outpasch  29233  lnopp2hpgb  29241  colopp  29247  elplngid  29260  lnincplng  29262  plngcp  29264  plngrot  29268  nhpmirhp  29276  lnperpexs  29310  ragraghl  29346  tgaaddcpbllem2  29350  tgaaddcpbllem3  29351  tgaaddcpbl2  29353  angmgmaddeu1  29379  angmgmaddcl  29391  prlnghpg  29424  prlngmo  29432  tgaltai  29445  erclwwlksym  30612  erclwwlktr  30613  erclwwlknsym  30661  erclwwlkntr  30662  eleclclwwlkn  30667  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  grpoidinvlem3  31108  ubthlem3  31474  norm1exi  31852  pjhthmo  31904  cdjreui  33034  cdj3i  33043  infxrge0glb  33357  mndlrinvb  33586  gsumwrd2dccatlem  33638  cyc3genpm  33713  isarchi3  33748  archiabl  33759  erler  33826  rlocisunit  33837  1arithidomlem1  34067  1arithidom  34069  1arithufdlem2  34077  1arithufdlem3  34078  1arithufd  34080  fldext2chn  34360  constrconj  34377  constrextdg2lem  34380  constrextdg2  34381  constrfiss  34383  zarclsun  34502  ordtrest2NEWlem  34554  lmxrge0  34584  esumcvg  34718  esum2d  34725  eulerpartlems  34992  eulerpartlemgvv  35008  onvf1odlem2  35883  connpconn  36000  cvmlift2lem12  36079  cvmlift2lem13  36080  cvmlift3lem2  36085  cvmlift3lem7  36090  cvmlift3  36093  fmlasuc  36151  fmla1  36152  satffunlem1lem1  36167  satffunlem2lem1  36169  r1peuqusdeg1  36408  funtransport  36796  funray  36905  funline  36907  fnessref  37145  neibastop2  37149  dissneqlem  38264  dissneq  38265  pibt2  38341  ptrest  38538  poimirlem27  38566  poimirlem32  38571  ismblfin  38580  volsupnfl  38584  itg2addnclem  38590  unirep  38649  filbcmb  38675  sdclem1  38678  sdc  38679  fdc  38680  incsequz  38683  heibor1lem  38744  heiborlem10  38755  isgrpda  38890  isdrngo2  38893  prnc  39002  prtlem13  39926  prtlem15  39933  lshpsmreu  40167  lshpkrlem1  40168  lshpkrlem3  40170  pclfinN  40958  4atex  41134  dihglblem2N  42352  lcfl7N  42559  lcf1o  42609  supinf  43294  fimgmcyclem  43598  mzpcompact2lem  43762  eldioph3  43777  diophrex  43786  rexrabdioph  43801  eldioph4i  43819  aomclem8  44063  hbtlem2  44126  rngunsnply  44171  onsucrn  44273  iunrelexpuztr  44719  ntrclsneine0lem  45064  rexlimddvcbvw  45204  cpcoll2d  45243  mnuprdlem3  45258  dvconstbi  45318  expgrowth  45319  wessf1ornlem  46200  rnmptlb  46255  rnmptbdd  46257  rnmptbd2  46261  rnmptbd  46268  rexabsle  46429  uzub  46441  infrpgernmpt  46475  limcperiod  46640  limsupre  46651  limsupbnd1f  46696  climinf2  46717  climinfmpt  46725  limsupubuzmpt  46729  limsupmnf  46731  limsupre2  46735  limsupmnfuzlem  46736  limsupmnfuz  46737  limsupre2mpt  46740  limsupre3  46743  limsupre3mpt  46744  limsupre3uz  46746  limsupreuz  46747  limsupreuzmpt  46749  supcnvlimsup  46750  climuz  46754  lmbr3  46757  climrescn  46758  limsuplt2  46763  liminflelimsup  46786  limsupgt  46788  liminfreuz  46813  liminflt  46815  xlimpnfxnegmnf  46824  xlimmnf  46851  xlimpnf  46852  xlimmnfmpt  46853  xlimpnfmpt  46854  dfxlim2  46858  cncfshiftioo  46902  itgiccshift  46990  itgperiod  46991  fourierdlem42  47159  fourierdlem48  47164  fourierdlem81  47197  fourierdlem92  47208  fourierdlem96  47212  fourierdlem97  47213  fourierdlem98  47214  fourierdlem99  47215  fourierdlem105  47221  fourierdlem108  47224  fourierdlem110  47226  fourierdlem112  47228  fourierdlem113  47229  meaiunincf  47493  meaiuninc3v  47494  hoidmvval0  47597  ovnhoi  47613  ovolval5lem3  47664  ovolval5  47665  smfsup  47824  smfinflem  47827  smfinf  47828  fsetsnfo  48123  2reuimp0  48184  nndivides2  48454  imaelsetpreimafv  48477  imasetpreimafvbijlemfo  48487  fundcmpsurinj  48491  fundcmpsurbijinj  48492  fmtnofac2lem  48653  2zlidl  49337  2zrngamgm  49342  2zrngagrp  49346  2zrngmmgm  49349  eenglngeehlnmlem1  49849  upciclem4  50277