Theorem cbvralvw 3241

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3352 with a disjoint variable condition, which does not require ax-10 2176, ax-11 2192, ax-12 2213, ax-13 2404. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2404. (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 2846	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 346	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2057	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3078	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3078	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 305	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1559   ∈ wcel 2143  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-clel 2838  df-ral 3078

This theorem is referenced by:  cbvraldva  3243  cbvral2vw  3245  cbvral3vw  3247  cbvral4vw  3248  reu7  3696  cbviinv  4998  disjxun  5099  reusv3i  5362  wereu2  5645  cnvpo  6275  frpomin  6328  f1mpt  7246  dfwe2  7758  tfinds  7841  frrlem1  8268  tfrlem1  8347  tfrlem12  8361  rdglem1  8387  tz7.48lem  8413  cbvixpv  8898  nneneq  9175  marypha1lem  9380  supub  9406  suplub  9407  ordtypecbv  9466  ordtypelem3  9469  ordtypelem9  9475  wemaplem1  9495  brwdom3  9531  ttrclss  9676  ttrclselem2  9682  tcrank  9843  infxpenc2  9979  aceq1  10074  aceq2  10076  dfac5  10086  dfac9  10094  dfac12lem3  10103  kmlem12  10119  kmlem14  10121  cofsmo  10227  infpssrlem4  10264  isfin3ds  10287  isf32lem2  10312  isf32lem11  10321  isf33lem  10324  domtriomlem  10400  axdc3  10412  zorn2lem7  10460  zorn2g  10461  fpwwe2cbv  10589  fpwwecbv  10603  pwfseq  10623  axgroth6  10787  dedekind  11347  suprleub  12159  infregelb  12177  nnsub  12258  uzwo  12913  ublbneg  12935  zsupss  12939  xrub  13316  fsuppmapnn0fiubex  14006  monoord2  14047  faclbnd4lem4  14310  bccl  14336  hashbc  14467  wrdind  14736  wrd2ind  14737  reuccatpfxs1  14761  cau3lem  15383  climmpt2  15601  caucvgrlem  15701  caurcvg2  15706  caucvgb  15708  fsum0diag2  15811  incexclem  15867  cvgrat  15914  mertenslem2  15916  mertens  15917  sqrt2irr  16282  gcdcllem1  16534  lcmfunsnlem1  16672  lcmfunsnlem2lem1  16673  prmind2  16720  prmpwdvds  16941  prmreclem5  16957  prmreclem6  16958  vdwlem7  17024  vdwlem10  17027  vdwlem13  17030  vdwnn  17035  ramcl  17066  isacs2  17686  catpropd  17742  chnind  18654  chnub  18655  grpinvalem  18708  grpinva  18709  gsumvalx  18711  mndind  18863  issubg4  19188  isnsg2  19198  elnmz  19205  gsmsymgreqlem2  19472  psgnunilem5  19535  psgnunilem3  19537  efgsdm  19771  gsummptnn0fzfv  20028  pgpfac1lem5  20122  pgpfac1  20123  pgpfac  20127  ablfaclem3  20130  lbsextg  21233  evlslem2  22133  mpfind  22169  cply1mul  22360  mdetuni0  22682  m2cpminvid2lem  22815  mp2pm2mplem4  22870  chcoeffeqlem  22946  cayhamlem3  22948  elcls3  23144  isclo2  23149  neiptopnei  23193  tgcn  23313  subbascn  23315  txcmplem2  23703  kqfvima  23791  kqt0lem  23797  isr0  23798  r0cld  23799  regr1lem2  23801  fbun  23901  flftg  24057  fclsbas  24082  alexsubALTlem2  24109  alexsubALTlem4  24111  ptcmplem4  24116  tsmsxplem1  24214  tsmsxp  24216  ustuqtop  24307  utopsnneip  24309  prdsxmslem2  24590  isclmp  25160  iscau4  25342  caucfil  25346  iscmet3  25356  bcthlem5  25391  bcth  25392  ovolicc2lem5  25584  uniioombllem6  25651  vitali  25676  ismbf3d  25717  itg1climres  25777  itg2seq  25805  itg2monolem1  25813  itg2mono  25816  rolle  26053  dvlipcn  26057  dvivthlem1  26071  ply1divex  26198  fta1g  26231  dgrco  26336  plydivex  26362  fta1  26373  vieta1  26377  ulmcaulem  26458  ulmcau  26459  abelthlem8  26503  wilth  27136  fta  27145  fsumdvdsmul  27260  dchrelbas3  27303  2sqlem6  27488  2sqlem10  27493  dchrisumlem3  27556  dchrisum  27557  dchrmusumlema  27558  dchrvmasumlema  27565  dchrisum0lema  27579  pntibndlem3  27657  pntlem3  27674  pntleml  27676  pnt3  27677  ostth2lem2  27699  ostth  27704  nosupcbv  27767  nosupdm  27769  nosupbnd1lem4  27776  nosupbnd2  27781  noinfcbv  27782  noinfdm  27784  noinfres  27787  noinfbnd1lem1  27788  noinfbnd2  27796  madebdayim  27982  madebday  27994  cofss  28024  coiniss  28025  cutminmax  28030  precsexlem9  28309  onsfi  28450  n0subs  28457  bdayfinbndcbv  28560  bdayfinbndlem2  28562  z12zsodd  28576  axcontlem1  29166  axcontlem6  29171  uspgr2wlkeq  29847  crctcshwlkn0  30022  frgrwopreglem5ALT  30525  grpoideu  30713  ubthlem3  31076  adjsym  32037  lnopunilem1  32214  elunop2  32217  lnophm  32223  cnlnadjlem5  32275  mdbr3  32501  mdbr4  32502  dmdbr3  32509  dmdbr4  32510  mddmd2  32513  fprodex01  33028  prodindf  33041  wrdt2ind  33132  toslublem  33151  tosglblem  33153  archiabl  33379  isarchiofld  33380  elrgspnlem1  33424  elrgspnlem2  33425  elrgspnlem4  33427  elrgspnsubrunlem2  33430  1arithidom  33734  1arithufdlem3  33743  vietadeg1  33876  vieta  33878  fedgmul  33929  fldextrspunlsplem  33971  constrconj  34043  qtophaus  34134  lmdvg  34251  esumcvg  34384  unelldsys  34456  ldgenpisyslem1  34461  eulerpartlemsv3  34659  eulerpartlemgvv  34674  signstfvneq0  34867  reprinfz1  34917  tgoldbachgtd  34957  bnj1185  35089  bnj222  35179  bnj517  35181  bnj1452  35348  bnj1463  35351  derangenlem  35522  subfacp1lem6  35536  subfacp1  35537  resconn  35597  cvmscbv  35609  sat1el2xp  35730  untangtr  36065  dfon2lem3  36134  dfon2lem7  36138  nn0prpwlem  36683  neibastop3  36723  fnemeet2  36728  weiunlem  36824  mh-infprim2bi  36908  mh-infprim3bi  36909  fvineqsnf1  37905  fvineqsneu  37906  pibt2  37912  phpreu  38104  poimirlem27  38147  heicant  38155  mblfinlem2  38158  ovoliunnfl  38162  voliunnfl  38164  mbfresfi  38166  upixp  38229  sdclem2  38242  fdc  38245  mettrifi  38257  heiborlem5  38315  heiborlem10  38320  heibor  38321  bfp  38324  disjressuc2  38911  cdleme25cv  40983  cdleme40v  41094  aks4d1p7  42701  aks6d1c1p3  42728  aks6d1c1p4  42729  supinf  42859  fsuppind  43173  mzpclval  43307  dford3lem1  43604  fnwe2lem1  43628  aomclem3  43634  aomclem4  43635  aomclem8  43639  dfac11  43640  hbtlem5  43706  nadd1suc  43970  ntrk2imkb  44614  ntrclsk2  44645  ntrclsk4  44649  fnchoice  45610  cncmpmax  45613  wessf1ornlem  45764  disjinfi  45771  rnmptbdd  45821  rnmptbd2  45825  rnmptbd  45832  supxrunb3  45975  unb2ltle  45990  monoord2xrv  46058  uzubioo2  46144  mccl  46175  climsuse  46185  limsupre  46216  limsuppnf  46286  limsupubuz  46288  limsupmnf  46296  limsupre2  46300  limsupmnfuz  46302  limsupre2mpt  46305  limsupre3  46308  limsupre3mpt  46309  limsupre3uzlem  46310  limsupre3uz  46311  limsupreuz  46312  limsupvaluz2  46313  limsupreuzmpt  46314  climuz  46319  lmbr3  46322  limsupge  46336  liminflelimsup  46351  liminfreuz  46378  xlimpnfxnegmnf  46389  cnrefiisp  46405  xlimmnf  46416  xlimpnf  46417  xlimmnfmpt  46418  xlimpnfmpt  46419  dfxlim2  46423  dvbdfbdioolem2  46504  dvbdfbdioo  46505  ioodvbdlimc1lem1  46506  ioodvbdlimc1lem2  46507  ioodvbdlimc2lem  46509  dvnprodlem3  46523  stoweidlem7  46582  stoweidlem15  46590  stoweidlem35  46610  wallispilem3  46642  fourierdlem68  46749  fourierdlem71  46752  fourierdlem73  46754  fourierdlem87  46768  fourierdlem100  46781  fourierdlem103  46784  fourierdlem104  46785  fourierdlem107  46788  fourierdlem109  46790  fourierdlem112  46793  etransc  46858  qndenserrnbllem  46869  dfsalgen2  46916  subsaliuncl  46933  meaiuninclem  47055  ovnsubaddlem2  47146  hoidmvlelem5  47174  hoidmvle  47175  hoiqssbllem3  47199  vonioo  47257  vonicc  47260  issmf  47303  issmfle  47320  issmfgt  47331  issmfge  47345  smfsuplem2  47387  chnerlem1  47459  2reuimp0  47709  uniimafveqt  47988  sbgoldbm  48407  mogoldbb  48408  bgoldbtbndlem4  48431  bgoldbtbnd  48432  nn0sumshdiglem1  49244  ipolub  49610  ipoglb  49613