Theorem cbvralvw 3212

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3332 with a disjoint variable condition, which does not require ax-10 2146, ax-11 2162, ax-12 2182, ax-13 2374. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2374. (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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2037	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3050	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3050	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2809  df-ral 3050

This theorem is referenced by:  cbvraldva  3214  cbvral2vw  3216  cbvral3vw  3218  cbvral4vw  3219  reu7  3688  cbviinv  4993  disjxun  5094  reusv3i  5347  wereu2  5619  cnvpo  6243  frpomin  6296  f1mpt  7205  dfwe2  7717  tfinds  7800  frrlem1  8226  tfrlem1  8305  tfrlem12  8318  rdglem1  8344  tz7.48lem  8370  cbvixpv  8851  nneneq  9128  marypha1lem  9334  supub  9360  suplub  9361  ordtypecbv  9420  ordtypelem3  9423  ordtypelem9  9429  wemaplem1  9449  brwdom3  9485  ttrclss  9627  ttrclselem2  9633  tcrank  9794  infxpenc2  9930  aceq1  10025  aceq2  10027  dfac5  10037  dfac9  10045  dfac12lem3  10054  kmlem12  10070  kmlem14  10072  cofsmo  10177  infpssrlem4  10214  isfin3ds  10237  isf32lem2  10262  isf32lem11  10271  isf33lem  10274  domtriomlem  10350  axdc3  10362  zorn2lem7  10410  zorn2g  10411  fpwwe2cbv  10539  fpwwecbv  10553  pwfseq  10573  axgroth6  10737  dedekind  11294  suprleub  12106  infregelb  12124  nnsub  12187  uzwo  12822  ublbneg  12844  zsupss  12848  xrub  13225  fsuppmapnn0fiubex  13913  monoord2  13954  faclbnd4lem4  14217  bccl  14243  hashbc  14374  wrdind  14643  wrd2ind  14644  reuccatpfxs1  14668  cau3lem  15276  climmpt2  15494  caucvgrlem  15594  caurcvg2  15599  caucvgb  15601  fsum0diag2  15704  incexclem  15757  cvgrat  15804  mertenslem2  15806  mertens  15807  sqrt2irr  16172  gcdcllem1  16424  lcmfunsnlem1  16562  lcmfunsnlem2lem1  16563  prmind2  16610  prmpwdvds  16830  prmreclem5  16846  prmreclem6  16847  vdwlem7  16913  vdwlem10  16916  vdwlem13  16919  vdwnn  16924  ramcl  16955  isacs2  17574  catpropd  17630  chnind  18542  chnub  18543  grpinvalem  18596  grpinva  18597  gsumvalx  18599  mndind  18751  issubg4  19073  isnsg2  19083  elnmz  19090  gsmsymgreqlem2  19358  psgnunilem5  19421  psgnunilem3  19423  efgsdm  19657  gsummptnn0fzfv  19914  pgpfac1lem5  20008  pgpfac1  20009  pgpfac  20013  ablfaclem3  20016  lbsextg  21115  evlslem2  22032  mpfind  22068  cply1mul  22238  mdetuni0  22563  m2cpminvid2lem  22696  mp2pm2mplem4  22751  chcoeffeqlem  22827  cayhamlem3  22829  elcls3  23025  isclo2  23030  neiptopnei  23074  tgcn  23194  subbascn  23196  txcmplem2  23584  kqfvima  23672  kqt0lem  23678  isr0  23679  r0cld  23680  regr1lem2  23682  fbun  23782  flftg  23938  fclsbas  23963  alexsubALTlem2  23990  alexsubALTlem4  23992  ptcmplem4  23997  tsmsxplem1  24095  tsmsxp  24097  ustuqtop  24188  utopsnneip  24190  prdsxmslem2  24471  isclmp  25051  iscau4  25233  caucfil  25237  iscmet3  25247  bcthlem5  25282  bcth  25283  ovolicc2lem5  25476  uniioombllem6  25543  vitali  25568  ismbf3d  25609  itg1climres  25669  itg2seq  25697  itg2monolem1  25705  itg2mono  25708  rolle  25948  dvlipcn  25953  dvivthlem1  25967  ply1divex  26096  fta1g  26129  dgrco  26235  plydivex  26259  fta1  26270  vieta1  26274  ulmcaulem  26357  ulmcau  26358  abelthlem8  26403  wilth  27035  fta  27044  fsumdvdsmul  27159  dchrelbas3  27203  2sqlem6  27388  2sqlem10  27393  dchrisumlem3  27456  dchrisum  27457  dchrmusumlema  27458  dchrvmasumlema  27465  dchrisum0lema  27479  pntibndlem3  27557  pntlem3  27574  pntleml  27576  pnt3  27577  ostth2lem2  27599  ostth  27604  nosupcbv  27668  nosupdm  27670  nosupbnd1lem4  27677  nosupbnd2  27682  noinfcbv  27683  noinfdm  27685  noinfres  27688  noinfbnd1lem1  27689  noinfbnd2  27697  madebdayim  27860  madebday  27872  cofss  27901  coiniss  27902  precsexlem9  28183  onsfi  28316  n0subs  28322  zs12zodd  28431  zs12bday  28433  axcontlem1  28986  axcontlem6  28991  uspgr2wlkeq  29668  crctcshwlkn0  29843  frgrwopreglem5ALT  30346  grpoideu  30533  ubthlem3  30896  adjsym  31857  lnopunilem1  32034  elunop2  32037  lnophm  32043  cnlnadjlem5  32095  mdbr3  32321  mdbr4  32322  dmdbr3  32329  dmdbr4  32330  mddmd2  32333  fprodex01  32855  prodindf  32893  wrdt2ind  32984  toslublem  33003  tosglblem  33005  archiabl  33229  isarchiofld  33230  elrgspnlem1  33273  elrgspnlem2  33274  elrgspnlem4  33276  elrgspnsubrunlem2  33279  1arithidom  33567  1arithufdlem3  33576  vietadeg1  33683  vieta  33685  fedgmul  33737  fldextrspunlsplem  33779  constrconj  33851  qtophaus  33942  lmdvg  34059  esumcvg  34192  unelldsys  34264  ldgenpisyslem1  34269  eulerpartlemsv3  34467  eulerpartlemgvv  34482  signstfvneq0  34678  reprinfz1  34728  tgoldbachgtd  34768  bnj1185  34898  bnj222  34988  bnj517  34990  bnj1452  35157  bnj1463  35160  derangenlem  35314  subfacp1lem6  35328  subfacp1  35329  resconn  35389  cvmscbv  35401  sat1el2xp  35522  untangtr  35857  dfon2lem3  35926  dfon2lem7  35930  nn0prpwlem  36465  neibastop3  36505  fnemeet2  36510  weiunlem2  36606  fvineqsnf1  37554  fvineqsneu  37555  pibt2  37561  phpreu  37744  poimirlem27  37787  heicant  37795  mblfinlem2  37798  ovoliunnfl  37802  voliunnfl  37804  mbfresfi  37806  upixp  37869  sdclem2  37882  fdc  37885  mettrifi  37897  heiborlem5  37955  heiborlem10  37960  heibor  37961  bfp  37964  disjressuc2  38535  cdleme25cv  40557  cdleme40v  40668  aks4d1p7  42276  aks6d1c1p3  42303  aks6d1c1p4  42304  supinf  42439  fsuppind  42775  mzpclval  42909  dford3lem1  43210  fnwe2lem1  43234  aomclem3  43240  aomclem4  43241  aomclem8  43245  dfac11  43246  hbtlem5  43312  nadd1suc  43576  ntrk2imkb  44220  ntrclsk2  44251  ntrclsk4  44255  fnchoice  45216  cncmpmax  45219  wessf1ornlem  45371  disjinfi  45378  rnmptbdd  45431  rnmptbd2  45435  rnmptbd  45442  supxrunb3  45585  unb2ltle  45601  monoord2xrv  45669  uzubioo2  45755  mccl  45786  climsuse  45796  limsupre  45827  limsuppnf  45897  limsupubuz  45899  limsupmnf  45907  limsupre2  45911  limsupmnfuz  45913  limsupre2mpt  45916  limsupre3  45919  limsupre3mpt  45920  limsupre3uzlem  45921  limsupre3uz  45922  limsupreuz  45923  limsupvaluz2  45924  limsupreuzmpt  45925  climuz  45930  lmbr3  45933  limsupge  45947  liminflelimsup  45962  liminfreuz  45989  xlimpnfxnegmnf  46000  cnrefiisp  46016  xlimmnf  46027  xlimpnf  46028  xlimmnfmpt  46029  xlimpnfmpt  46030  dfxlim2  46034  dvbdfbdioolem2  46115  dvbdfbdioo  46116  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnprodlem3  46134  stoweidlem7  46193  stoweidlem15  46201  stoweidlem35  46221  wallispilem3  46253  fourierdlem68  46360  fourierdlem71  46363  fourierdlem73  46365  fourierdlem87  46379  fourierdlem100  46392  fourierdlem103  46395  fourierdlem104  46396  fourierdlem107  46399  fourierdlem109  46401  fourierdlem112  46404  etransc  46469  qndenserrnbllem  46480  dfsalgen2  46527  subsaliuncl  46544  meaiuninclem  46666  ovnsubaddlem2  46757  hoidmvlelem5  46785  hoidmvle  46786  hoiqssbllem3  46810  vonioo  46868  vonicc  46871  issmf  46914  issmfle  46931  issmfgt  46942  issmfge  46956  smfsuplem2  46998  chnerlem1  47068  2reuimp0  47302  uniimafveqt  47569  sbgoldbm  47972  mogoldbb  47973  bgoldbtbndlem4  47996  bgoldbtbnd  47997  nn0sumshdiglem1  48809  ipolub  49175  ipoglb  49178