Theorem cbvrexvw 3214

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

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

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 2008  ax-8 2111

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

This theorem is referenced by:  cbvrex2vw  3218  reu7  3700  cbviunv  4999  disjiund  5093  reusv3  5355  xpdifid  6129  fliftfun  7269  funcnvuni  7888  fiunlem  7900  poseq  8114  soseq  8115  nneob  8597  coflton  8612  cofon1  8613  cofon2  8614  pssnn  9109  frfi  9208  finsschain  9286  marypha1lem  9360  supmo  9379  suplub2  9388  infmo  9424  ordtypelem3  9449  ordtypelem9  9455  wemaplem1  9475  brwdom3  9511  unwdomg  9513  cantnf  9622  ttrcltr  9645  trcl  9657  infxpenc2  9951  aceq2  10048  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem9  10088  kmlem14  10093  fin23lem26  10254  fin1a2lem13  10341  axdc3lem3  10381  winainflem  10622  axgroth4  10761  suprlub  12123  supaddc  12126  supadd  12127  supmul1  12128  supmullem1  12129  supmullem2  12130  supmul  12131  ublbneg  12868  zsupss  12872  xrsupsslem  13243  xrinfmsslem  13244  rexanre  15289  rexuzre  15295  rexico  15296  caurcvg2  15620  caucvgb  15622  summolem2  15658  summo  15659  mertens  15828  prodmolem2  15877  prodmo  15878  odd2np1lem  16286  gcdcllem1  16445  prmdvdsncoprmbd  16673  pceu  16793  4sqlem12  16903  vdwlem10  16937  vdwlem13  16940  vdwnn  16945  drsdirfi  18242  grprida  18578  smndex1mgm  18810  smndex1mndlem  18812  dfgrp2  18870  dfgrp3lem  18946  cyccom  19111  gaorb  19215  psgnunilem3  19402  psgnunilem4  19403  psgneu  19412  pj1eu  19602  efgsfo  19645  cyggeninv  19789  cygabl  19797  pgpfac1lem5  19987  pgpfac1  19988  pgpfaclem2  19990  lss1d  20845  lspsneq  21008  lspsolvlem  21028  lbsextlem2  21045  cygznlem3  21455  mplcoe5lem  21922  pmatcollpw3fi1lem2  22650  ordtrest2lem  23066  cnprest  23152  1stcfb  23308  1stcelcls  23324  elpt  23435  fbssfi  23700  fgcl  23741  rnelfmlem  23815  fmfnfmlem3  23819  txflf  23869  alexsubb  23909  alexsubALTlem4  23913  isucn2  24142  icccmplem2  24688  ply1divex  26018  coeeu  26106  plydivex  26181  aannenlem2  26213  ulmcau  26280  ulmbdd  26283  dchrptlem2  27152  bposlem9  27179  2lgslem1b  27279  pntibndlem3  27479  pntlemi  27491  pntlemp  27497  pntleml  27498  pnt3  27499  nosupprefixmo  27588  noinfprefixmo  27589  nosupcbv  27590  nosupdm  27592  nosupfv  27594  nosupres  27595  nosupbnd1lem1  27596  nosupbnd1lem4  27599  noinfcbv  27605  noinfdm  27607  noinfbnd1lem4  27614  cofsslt  27802  coinitsslt  27803  addsval2  27846  addscut  27861  addsunif  27885  norecdiv  28069  recsne0  28071  bdayn0sf1o  28235  dfnns2  28237  n0seo  28283  pw2recs  28299  recut  28323  readdscl  28326  legval  28487  legov  28488  legov2  28489  outpasch  28658  lnopp2hpgb  28666  colopp  28672  erclwwlksym  29923  erclwwlktr  29924  erclwwlknsym  29972  erclwwlkntr  29973  eleclclwwlkn  29978  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  grpoidinvlem3  30408  ubthlem3  30774  norm1exi  31152  pjhthmo  31204  cdjreui  32334  cdj3i  32343  infxrge0glb  32661  mndlrinvb  32939  gsumwrd2dccatlem  32979  cyc3genpm  33082  isarchi3  33114  archiabl  33125  erler  33189  isdrng4  33218  1arithidomlem1  33479  1arithidom  33481  1arithufdlem2  33489  1arithufdlem3  33490  1arithufd  33492  fldext2chn  33691  constrconj  33708  constrextdg2lem  33711  constrextdg2  33712  constrfiss  33714  zarclsun  33833  ordtrest2NEWlem  33885  lmxrge0  33915  esumcvg  34049  esum2d  34056  eulerpartlems  34324  eulerpartlemgvv  34340  onvf1odlem2  35064  connpconn  35195  cvmlift2lem12  35274  cvmlift2lem13  35275  cvmlift3lem2  35280  cvmlift3lem7  35285  cvmlift3  35288  fmlasuc  35346  fmla1  35347  satffunlem1lem1  35362  satffunlem2lem1  35364  r1peuqusdeg1  35603  funtransport  35992  funray  36101  funline  36103  fnessref  36318  neibastop2  36322  dissneqlem  37301  dissneq  37302  pibt2  37378  ptrest  37586  poimirlem27  37614  poimirlem32  37619  ismblfin  37628  volsupnfl  37632  itg2addnclem  37638  unirep  37681  filbcmb  37707  sdclem1  37710  sdc  37711  fdc  37712  incsequz  37715  heibor1lem  37776  heiborlem10  37787  isgrpda  37922  isdrngo2  37925  prnc  38034  prtlem13  38834  prtlem15  38841  lshpsmreu  39075  lshpkrlem1  39076  lshpkrlem3  39078  pclfinN  39867  4atex  40043  dihglblem2N  41261  lcfl7N  41468  lcf1o  41518  supinf  42203  fimgmcyclem  42494  mzpcompact2lem  42712  eldioph3  42727  diophrex  42736  rexrabdioph  42755  eldioph4i  42773  aomclem8  43023  hbtlem2  43086  rngunsnply  43131  onsucrn  43233  iunrelexpuztr  43681  ntrclsneine0lem  44026  rexlimddvcbvw  44168  cpcoll2d  44221  mnuprdlem3  44236  dvconstbi  44296  expgrowth  44297  wessf1ornlem  45152  rnmptlb  45210  rnmptbdd  45212  rnmptbd2  45216  rnmptbd  45223  rexabsle  45388  uzub  45400  infrpgernmpt  45434  limcperiod  45599  limsupre  45612  limsupbnd1f  45657  climinf2  45678  climinfmpt  45686  limsupubuzmpt  45690  limsupmnf  45692  limsupre2  45696  limsupmnfuzlem  45697  limsupmnfuz  45698  limsupre2mpt  45701  limsupre3  45704  limsupre3mpt  45705  limsupre3uz  45707  limsupreuz  45708  limsupreuzmpt  45710  supcnvlimsup  45711  climuz  45715  lmbr3  45718  climrescn  45719  limsuplt2  45724  liminflelimsup  45747  limsupgt  45749  liminfreuz  45774  liminflt  45776  xlimpnfxnegmnf  45785  xlimmnf  45812  xlimpnf  45813  xlimmnfmpt  45814  xlimpnfmpt  45815  dfxlim2  45819  cncfshiftioo  45863  itgiccshift  45951  itgperiod  45952  fourierdlem42  46120  fourierdlem48  46125  fourierdlem81  46158  fourierdlem92  46169  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem105  46182  fourierdlem108  46185  fourierdlem110  46187  fourierdlem112  46189  fourierdlem113  46190  meaiunincf  46454  meaiuninc3v  46455  hoidmvval0  46558  ovnhoi  46574  ovolval5lem3  46625  ovolval5  46626  smfsup  46785  smfinflem  46788  smfinf  46789  fsetsnfo  47027  2reuimp0  47088  imaelsetpreimafv  47369  imasetpreimafvbijlemfo  47379  fundcmpsurinj  47383  fundcmpsurbijinj  47384  fmtnofac2lem  47542  2zlidl  48201  2zrngamgm  48206  2zrngagrp  48210  2zrngmmgm  48213  eenglngeehlnmlem1  48699  upciclem4  49131