Theorem cbvralvw 3215

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-ral 3052

This theorem is referenced by:  cbvraldva  3217  cbvral2vw  3219  cbvral3vw  3221  cbvral4vw  3222  reu7  3678  cbviinv  4982  disjxun  5083  reusv3i  5346  wereu2  5628  cnvpo  6251  frpomin  6304  f1mpt  7216  dfwe2  7728  tfinds  7811  frrlem1  8236  tfrlem1  8315  tfrlem12  8328  rdglem1  8354  tz7.48lem  8380  cbvixpv  8863  nneneq  9140  marypha1lem  9346  supub  9372  suplub  9373  ordtypecbv  9432  ordtypelem3  9435  ordtypelem9  9441  wemaplem1  9461  brwdom3  9497  ttrclss  9641  ttrclselem2  9647  tcrank  9808  infxpenc2  9944  aceq1  10039  aceq2  10041  dfac5  10051  dfac9  10059  dfac12lem3  10068  kmlem12  10084  kmlem14  10086  cofsmo  10191  infpssrlem4  10228  isfin3ds  10251  isf32lem2  10276  isf32lem11  10285  isf33lem  10288  domtriomlem  10364  axdc3  10376  zorn2lem7  10424  zorn2g  10425  fpwwe2cbv  10553  fpwwecbv  10567  pwfseq  10587  axgroth6  10751  dedekind  11309  suprleub  12122  infregelb  12140  nnsub  12221  uzwo  12861  ublbneg  12883  zsupss  12887  xrub  13264  fsuppmapnn0fiubex  13954  monoord2  13995  faclbnd4lem4  14258  bccl  14284  hashbc  14415  wrdind  14684  wrd2ind  14685  reuccatpfxs1  14709  cau3lem  15317  climmpt2  15535  caucvgrlem  15635  caurcvg2  15640  caucvgb  15642  fsum0diag2  15745  incexclem  15801  cvgrat  15848  mertenslem2  15850  mertens  15851  sqrt2irr  16216  gcdcllem1  16468  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  prmind2  16654  prmpwdvds  16875  prmreclem5  16891  prmreclem6  16892  vdwlem7  16958  vdwlem10  16961  vdwlem13  16964  vdwnn  16969  ramcl  17000  isacs2  17619  catpropd  17675  chnind  18587  chnub  18588  grpinvalem  18641  grpinva  18642  gsumvalx  18644  mndind  18796  issubg4  19121  isnsg2  19131  elnmz  19138  gsmsymgreqlem2  19406  psgnunilem5  19469  psgnunilem3  19471  efgsdm  19705  gsummptnn0fzfv  19962  pgpfac1lem5  20056  pgpfac1  20057  pgpfac  20061  ablfaclem3  20064  lbsextg  21160  evlslem2  22057  mpfind  22093  cply1mul  22261  mdetuni0  22586  m2cpminvid2lem  22719  mp2pm2mplem4  22774  chcoeffeqlem  22850  cayhamlem3  22852  elcls3  23048  isclo2  23053  neiptopnei  23097  tgcn  23217  subbascn  23219  txcmplem2  23607  kqfvima  23695  kqt0lem  23701  isr0  23702  r0cld  23703  regr1lem2  23705  fbun  23805  flftg  23961  fclsbas  23986  alexsubALTlem2  24013  alexsubALTlem4  24015  ptcmplem4  24020  tsmsxplem1  24118  tsmsxp  24120  ustuqtop  24211  utopsnneip  24213  prdsxmslem2  24494  isclmp  25064  iscau4  25246  caucfil  25250  iscmet3  25260  bcthlem5  25295  bcth  25296  ovolicc2lem5  25488  uniioombllem6  25555  vitali  25580  ismbf3d  25621  itg1climres  25681  itg2seq  25709  itg2monolem1  25717  itg2mono  25720  rolle  25957  dvlipcn  25961  dvivthlem1  25975  ply1divex  26102  fta1g  26135  dgrco  26240  plydivex  26263  fta1  26274  vieta1  26278  ulmcaulem  26359  ulmcau  26360  abelthlem8  26404  wilth  27034  fta  27043  fsumdvdsmul  27158  dchrelbas3  27201  2sqlem6  27386  2sqlem10  27391  dchrisumlem3  27454  dchrisum  27455  dchrmusumlema  27456  dchrvmasumlema  27463  dchrisum0lema  27477  pntibndlem3  27555  pntlem3  27572  pntleml  27574  pnt3  27575  ostth2lem2  27597  ostth  27602  nosupcbv  27666  nosupdm  27668  nosupbnd1lem4  27675  nosupbnd2  27680  noinfcbv  27681  noinfdm  27683  noinfres  27686  noinfbnd1lem1  27687  noinfbnd2  27695  madebdayim  27880  madebday  27892  cofss  27922  coiniss  27923  cutminmax  27928  precsexlem9  28207  onsfi  28348  n0subs  28355  bdayfinbndcbv  28458  bdayfinbndlem2  28460  z12zsodd  28474  axcontlem1  29033  axcontlem6  29038  uspgr2wlkeq  29714  crctcshwlkn0  29889  frgrwopreglem5ALT  30392  grpoideu  30580  ubthlem3  30943  adjsym  31904  lnopunilem1  32081  elunop2  32084  lnophm  32090  cnlnadjlem5  32142  mdbr3  32368  mdbr4  32369  dmdbr3  32376  dmdbr4  32377  mddmd2  32380  fprodex01  32898  prodindf  32922  wrdt2ind  33013  toslublem  33032  tosglblem  33034  archiabl  33259  isarchiofld  33260  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  1arithidom  33597  1arithufdlem3  33606  vietadeg1  33722  vieta  33724  fedgmul  33775  fldextrspunlsplem  33817  constrconj  33889  qtophaus  33980  lmdvg  34097  esumcvg  34230  unelldsys  34302  ldgenpisyslem1  34307  eulerpartlemsv3  34505  eulerpartlemgvv  34520  signstfvneq0  34716  reprinfz1  34766  tgoldbachgtd  34806  bnj1185  34935  bnj222  35025  bnj517  35027  bnj1452  35194  bnj1463  35197  derangenlem  35353  subfacp1lem6  35367  subfacp1  35368  resconn  35428  cvmscbv  35440  sat1el2xp  35561  untangtr  35896  dfon2lem3  35965  dfon2lem7  35969  nn0prpwlem  36504  neibastop3  36544  fnemeet2  36549  weiunlem  36645  mh-infprim2bi  36729  mh-infprim3bi  36730  fvineqsnf1  37726  fvineqsneu  37727  pibt2  37733  phpreu  37925  poimirlem27  37968  heicant  37976  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  mbfresfi  37987  upixp  38050  sdclem2  38063  fdc  38066  mettrifi  38078  heiborlem5  38136  heiborlem10  38141  heibor  38142  bfp  38145  disjressuc2  38732  cdleme25cv  40804  cdleme40v  40915  aks4d1p7  42522  aks6d1c1p3  42549  aks6d1c1p4  42550  supinf  42681  fsuppind  43023  mzpclval  43157  dford3lem1  43454  fnwe2lem1  43478  aomclem3  43484  aomclem4  43485  aomclem8  43489  dfac11  43490  hbtlem5  43556  nadd1suc  43820  ntrk2imkb  44464  ntrclsk2  44495  ntrclsk4  44499  fnchoice  45460  cncmpmax  45463  wessf1ornlem  45615  disjinfi  45622  rnmptbdd  45674  rnmptbd2  45678  rnmptbd  45685  supxrunb3  45828  unb2ltle  45843  monoord2xrv  45911  uzubioo2  45997  mccl  46028  climsuse  46038  limsupre  46069  limsuppnf  46139  limsupubuz  46141  limsupmnf  46149  limsupre2  46153  limsupmnfuz  46155  limsupre2mpt  46158  limsupre3  46161  limsupre3mpt  46162  limsupre3uzlem  46163  limsupre3uz  46164  limsupreuz  46165  limsupvaluz2  46166  limsupreuzmpt  46167  climuz  46172  lmbr3  46175  limsupge  46189  liminflelimsup  46204  liminfreuz  46231  xlimpnfxnegmnf  46242  cnrefiisp  46258  xlimmnf  46269  xlimpnf  46270  xlimmnfmpt  46271  xlimpnfmpt  46272  dfxlim2  46276  dvbdfbdioolem2  46357  dvbdfbdioo  46358  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem3  46376  stoweidlem7  46435  stoweidlem15  46443  stoweidlem35  46463  wallispilem3  46495  fourierdlem68  46602  fourierdlem71  46605  fourierdlem73  46607  fourierdlem87  46621  fourierdlem100  46634  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem109  46643  fourierdlem112  46646  etransc  46711  qndenserrnbllem  46722  dfsalgen2  46769  subsaliuncl  46786  meaiuninclem  46908  ovnsubaddlem2  46999  hoidmvlelem5  47027  hoidmvle  47028  hoiqssbllem3  47052  vonioo  47110  vonicc  47113  issmf  47156  issmfle  47173  issmfgt  47184  issmfge  47198  smfsuplem2  47240  chnerlem1  47312  2reuimp0  47562  uniimafveqt  47841  sbgoldbm  48260  mogoldbb  48261  bgoldbtbndlem4  48284  bgoldbtbnd  48285  nn0sumshdiglem1  49097  ipolub  49463  ipoglb  49466