Theorem cbvralvw 3217

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3328 with a disjoint variable condition, which does not require ax-10 2152, ax-11 2168, ax-12 2189, ax-13 2380. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2380. (Revised by GG, 10-Jan-2024.)

Hypothesis

Ref	Expression
cbvralvw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvralvw	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvralvw

Step	Hyp	Ref	Expression
1		eleq1w 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 345	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2043	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3054	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3054	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 304	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814  df-ral 3054

This theorem is referenced by:  cbvraldva  3219  cbvral2vw  3221  cbvral3vw  3223  cbvral4vw  3224  reu7  3673  cbviinv  4969  disjxun  5070  reusv3i  5333  wereu2  5615  cnvpo  6238  frpomin  6291  f1mpt  7205  dfwe2  7717  tfinds  7800  frrlem1  8226  tfrlem1  8305  tfrlem12  8318  rdglem1  8344  tz7.48lem  8370  cbvixpv  8853  nneneq  9130  marypha1lem  9336  supub  9362  suplub  9363  ordtypecbv  9422  ordtypelem3  9425  ordtypelem9  9431  wemaplem1  9451  brwdom3  9487  ttrclss  9632  ttrclselem2  9638  tcrank  9799  infxpenc2  9935  aceq1  10030  aceq2  10032  dfac5  10042  dfac9  10050  dfac12lem3  10059  kmlem12  10075  kmlem14  10077  cofsmo  10182  infpssrlem4  10219  isfin3ds  10242  isf32lem2  10267  isf32lem11  10276  isf33lem  10279  domtriomlem  10355  axdc3  10367  zorn2lem7  10415  zorn2g  10416  fpwwe2cbv  10544  fpwwecbv  10558  pwfseq  10578  axgroth6  10742  dedekind  11300  suprleub  12113  infregelb  12131  nnsub  12212  uzwo  12852  ublbneg  12874  zsupss  12878  xrub  13255  fsuppmapnn0fiubex  13945  monoord2  13986  faclbnd4lem4  14249  bccl  14275  hashbc  14406  wrdind  14675  wrd2ind  14676  reuccatpfxs1  14700  cau3lem  15308  climmpt2  15526  caucvgrlem  15626  caurcvg2  15631  caucvgb  15633  fsum0diag2  15736  incexclem  15792  cvgrat  15839  mertenslem2  15841  mertens  15842  sqrt2irr  16207  gcdcllem1  16459  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  prmind2  16645  prmpwdvds  16866  prmreclem5  16882  prmreclem6  16883  vdwlem7  16949  vdwlem10  16952  vdwlem13  16955  vdwnn  16960  ramcl  16991  isacs2  17610  catpropd  17666  chnind  18578  chnub  18579  grpinvalem  18632  grpinva  18633  gsumvalx  18635  mndind  18787  issubg4  19112  isnsg2  19122  elnmz  19129  gsmsymgreqlem2  19397  psgnunilem5  19460  psgnunilem3  19462  efgsdm  19696  gsummptnn0fzfv  19953  pgpfac1lem5  20047  pgpfac1  20048  pgpfac  20052  ablfaclem3  20055  lbsextg  21155  evlslem2  22055  mpfind  22091  cply1mul  22282  mdetuni0  22604  m2cpminvid2lem  22737  mp2pm2mplem4  22792  chcoeffeqlem  22868  cayhamlem3  22870  elcls3  23066  isclo2  23071  neiptopnei  23115  tgcn  23235  subbascn  23237  txcmplem2  23625  kqfvima  23713  kqt0lem  23719  isr0  23720  r0cld  23721  regr1lem2  23723  fbun  23823  flftg  23979  fclsbas  24004  alexsubALTlem2  24031  alexsubALTlem4  24033  ptcmplem4  24038  tsmsxplem1  24136  tsmsxp  24138  ustuqtop  24229  utopsnneip  24231  prdsxmslem2  24512  isclmp  25082  iscau4  25264  caucfil  25268  iscmet3  25278  bcthlem5  25313  bcth  25314  ovolicc2lem5  25506  uniioombllem6  25573  vitali  25598  ismbf3d  25639  itg1climres  25699  itg2seq  25727  itg2monolem1  25735  itg2mono  25738  rolle  25975  dvlipcn  25979  dvivthlem1  25993  ply1divex  26120  fta1g  26153  dgrco  26258  plydivex  26281  fta1  26292  vieta1  26296  ulmcaulem  26377  ulmcau  26378  abelthlem8  26422  wilth  27052  fta  27061  fsumdvdsmul  27176  dchrelbas3  27219  2sqlem6  27404  2sqlem10  27409  dchrisumlem3  27472  dchrisum  27473  dchrmusumlema  27474  dchrvmasumlema  27481  dchrisum0lema  27495  pntibndlem3  27573  pntlem3  27590  pntleml  27592  pnt3  27593  ostth2lem2  27615  ostth  27620  nosupcbv  27684  nosupdm  27686  nosupbnd1lem4  27693  nosupbnd2  27698  noinfcbv  27699  noinfdm  27701  noinfres  27704  noinfbnd1lem1  27705  noinfbnd2  27713  madebdayim  27898  madebday  27910  cofss  27940  coiniss  27941  cutminmax  27946  precsexlem9  28225  onsfi  28366  n0subs  28373  bdayfinbndcbv  28476  bdayfinbndlem2  28478  z12zsodd  28492  axcontlem1  29051  axcontlem6  29056  uspgr2wlkeq  29732  crctcshwlkn0  29907  frgrwopreglem5ALT  30410  grpoideu  30598  ubthlem3  30961  adjsym  31922  lnopunilem1  32099  elunop2  32102  lnophm  32108  cnlnadjlem5  32160  mdbr3  32386  mdbr4  32387  dmdbr3  32394  dmdbr4  32395  mddmd2  32398  fprodex01  32917  prodindf  32941  wrdt2ind  33032  toslublem  33051  tosglblem  33053  archiabl  33279  isarchiofld  33280  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem4  33326  elrgspnsubrunlem2  33329  1arithidom  33620  1arithufdlem3  33629  vietadeg1  33762  vieta  33764  fedgmul  33815  fldextrspunlsplem  33857  constrconj  33929  qtophaus  34020  lmdvg  34137  esumcvg  34270  unelldsys  34342  ldgenpisyslem1  34347  eulerpartlemsv3  34545  eulerpartlemgvv  34560  signstfvneq0  34756  reprinfz1  34806  tgoldbachgtd  34846  bnj1185  34975  bnj222  35065  bnj517  35067  bnj1452  35234  bnj1463  35237  derangenlem  35399  subfacp1lem6  35413  subfacp1  35414  resconn  35474  cvmscbv  35486  sat1el2xp  35607  untangtr  35942  dfon2lem3  36011  dfon2lem7  36015  nn0prpwlem  36550  neibastop3  36590  fnemeet2  36595  weiunlem  36691  mh-infprim2bi  36775  mh-infprim3bi  36776  fvineqsnf1  37772  fvineqsneu  37773  pibt2  37779  phpreu  37971  poimirlem27  38014  heicant  38022  mblfinlem2  38025  ovoliunnfl  38029  voliunnfl  38031  mbfresfi  38033  upixp  38096  sdclem2  38109  fdc  38112  mettrifi  38124  heiborlem5  38182  heiborlem10  38187  heibor  38188  bfp  38191  disjressuc2  38778  cdleme25cv  40850  cdleme40v  40961  aks4d1p7  42568  aks6d1c1p3  42595  aks6d1c1p4  42596  supinf  42726  fsuppind  43040  mzpclval  43174  dford3lem1  43471  fnwe2lem1  43495  aomclem3  43501  aomclem4  43502  aomclem8  43506  dfac11  43507  hbtlem5  43573  nadd1suc  43837  ntrk2imkb  44481  ntrclsk2  44512  ntrclsk4  44516  fnchoice  45477  cncmpmax  45480  wessf1ornlem  45632  disjinfi  45639  rnmptbdd  45689  rnmptbd2  45693  rnmptbd  45700  supxrunb3  45843  unb2ltle  45858  monoord2xrv  45926  uzubioo2  46012  mccl  46043  climsuse  46053  limsupre  46084  limsuppnf  46154  limsupubuz  46156  limsupmnf  46164  limsupre2  46168  limsupmnfuz  46170  limsupre2mpt  46173  limsupre3  46176  limsupre3mpt  46177  limsupre3uzlem  46178  limsupre3uz  46179  limsupreuz  46180  limsupvaluz2  46181  limsupreuzmpt  46182  climuz  46187  lmbr3  46190  limsupge  46204  liminflelimsup  46219  liminfreuz  46246  xlimpnfxnegmnf  46257  cnrefiisp  46273  xlimmnf  46284  xlimpnf  46285  xlimmnfmpt  46286  xlimpnfmpt  46287  dfxlim2  46291  dvbdfbdioolem2  46372  dvbdfbdioo  46373  ioodvbdlimc1lem1  46374  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnprodlem3  46391  stoweidlem7  46450  stoweidlem15  46458  stoweidlem35  46478  wallispilem3  46510  fourierdlem68  46617  fourierdlem71  46620  fourierdlem73  46622  fourierdlem87  46636  fourierdlem100  46649  fourierdlem103  46652  fourierdlem104  46653  fourierdlem107  46656  fourierdlem109  46658  fourierdlem112  46661  etransc  46726  qndenserrnbllem  46737  dfsalgen2  46784  subsaliuncl  46801  meaiuninclem  46923  ovnsubaddlem2  47014  hoidmvlelem5  47042  hoidmvle  47043  hoiqssbllem3  47067  vonioo  47125  vonicc  47128  issmf  47171  issmfle  47188  issmfgt  47199  issmfge  47213  smfsuplem2  47255  chnerlem1  47327  2reuimp0  47577  uniimafveqt  47856  sbgoldbm  48275  mogoldbb  48276  bgoldbtbndlem4  48299  bgoldbtbnd  48300  nn0sumshdiglem1  49112  ipolub  49478  ipoglb  49481