Theorem cbvralvw 3243

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3353 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 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2066	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3080	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3080	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 306	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2143  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ral 3080

This theorem is referenced by:  cbvraldva  3245  cbvral2vw  3247  cbvral3vw  3249  cbvral4vw  3250  reu7  3695  cbviinv  5004  disjxun  5107  reusv3i  5375  wereu2  5658  cnvpo  6288  frpomin  6341  f1mpt  7259  dfwe2  7769  tfinds  7852  frrlem1  8279  tfrlem1  8358  tfrlem12  8372  rdglem1  8398  tz7.48lem  8424  cbvixpv  8909  nneneq  9186  marypha1lem  9389  supub  9415  suplub  9416  ordtypecbv  9475  ordtypelem3  9478  ordtypelem9  9484  wemaplem1  9504  brwdom3  9540  ttrclss  9685  ttrclselem2  9691  tcrank  9852  infxpenc2  10002  aceq1  10097  aceq2  10099  dfac5  10108  dfac9  10116  dfac12lem3  10125  kmlem12  10141  kmlem14  10143  cofsmo  10248  infpssrlem4  10285  isfin3ds  10308  isf32lem2  10333  isf32lem11  10342  isf33lem  10345  domtriomlem  10421  axdc3  10433  zorn2lem7  10481  zorn2g  10482  fpwwe2cbv  10610  fpwwecbv  10624  pwfseq  10644  axgroth6  10808  dedekind  11368  suprleub  12176  infregelb  12194  nnsub  12275  uzwo  12930  ublbneg  12952  zsupss  12956  xrub  13333  fsuppmapnn0fiubex  14024  monoord2  14065  faclbnd4lem4  14328  bccl  14354  hashbc  14486  wrdind  14755  wrd2ind  14756  reuccatpfxs1  14780  cau3lem  15402  climmpt2  15620  caucvgrlem  15720  caurcvg2  15725  caucvgb  15727  fsum0diag2  15830  incexclem  15886  cvgrat  15933  mertenslem2  15935  mertens  15936  sqrt2irr  16300  gcdcllem1  16552  lcmfunsnlem1  16690  lcmfunsnlem2lem1  16691  prmind2  16738  prmpwdvds  16959  prmreclem5  16975  prmreclem6  16976  vdwlem7  17042  vdwlem10  17045  vdwlem13  17048  vdwnn  17053  ramcl  17084  isacs2  17704  catpropd  17760  chnind  18672  chnub  18673  grpinvalem  18726  grpinva  18727  gsumvalx  18729  mndind  18882  issubg4  19207  isnsg2  19217  elnmz  19224  gsmsymgreqlem2  19496  psgnunilem5  19559  psgnunilem3  19561  efgsdm  19795  gsummptnn0fzfv  20052  pgpfac1lem5  20146  pgpfac1  20147  pgpfac  20151  ablfaclem3  20154  lbsextg  21286  evlslem2  22230  mpfind  22266  cply1mul  22456  mdetuni0  22778  m2cpminvid2lem  22911  mp2pm2mplem4  22966  chcoeffeqlem  23042  cayhamlem3  23044  elcls3  23240  isclo2  23245  neiptopnei  23289  tgcn  23409  subbascn  23411  txcmplem2  23799  kqfvima  23887  kqt0lem  23893  isr0  23894  r0cld  23895  regr1lem2  23897  fbun  23997  flftg  24153  fclsbas  24178  alexsubALTlem2  24205  alexsubALTlem4  24207  ptcmplem4  24212  tsmsxplem1  24310  tsmsxp  24312  ustuqtop  24403  utopsnneip  24405  prdsxmslem2  24686  isclmp  25256  iscau4  25438  caucfil  25442  iscmet3  25452  bcthlem5  25487  bcth  25488  ovolicc2lem5  25680  uniioombllem6  25747  vitali  25772  ismbf3d  25813  itg1climres  25873  itg2seq  25901  itg2monolem1  25909  itg2mono  25912  rolle  26149  dvlipcn  26153  dvivthlem1  26167  ply1divex  26294  fta1g  26327  dgrco  26432  plydivex  26458  fta1  26469  vieta1  26473  ulmcaulem  26557  ulmcau  26558  abelthlem8  26602  wilth  27235  fta  27244  fsumdvdsmul  27359  dchrelbas3  27402  2sqlem6  27587  2sqlem10  27592  dchrisumlem3  27655  dchrisum  27656  dchrmusumlema  27657  dchrvmasumlema  27664  dchrisum0lema  27678  pntibndlem3  27756  pntlem3  27773  pntleml  27775  pnt3  27776  ostth2lem2  27798  ostth  27803  nosupcbv  27866  nosupdm  27868  nosupbnd1lem4  27875  nosupbnd2  27880  noinfcbv  27881  noinfdm  27883  noinfres  27886  noinfbnd1lem1  27887  noinfbnd2  27895  madebdayim  28081  madebday  28093  cofss  28123  coiniss  28124  cutminmax  28129  precsexlem9  28408  onsfi  28549  n0subs  28556  bdayfinbndcbv  28659  bdayfinbndlem2  28661  z12zsodd  28675  axcontlem1  29314  axcontlem6  29319  uspgr2wlkeq  29995  crctcshwlkn0  30170  frgrwopreglem5ALT  30673  grpoideu  30861  ubthlem3  31224  adjsym  32185  lnopunilem1  32362  elunop2  32365  lnophm  32371  cnlnadjlem5  32423  mdbr3  32649  mdbr4  32650  dmdbr3  32657  dmdbr4  32658  mddmd2  32661  fprodex01  33169  prodindf  33182  wrdt2ind  33273  toslublem  33292  tosglblem  33294  archiabl  33518  isarchiofld  33519  elrgspnlem1  33562  elrgspnlem2  33563  elrgspnlem4  33565  elrgspnsubrunlem2  33568  1arithidom  33827  1arithufdlem3  33836  vietadeg1  33968  vieta  33970  fedgmul  34021  fldextrspunlsplem  34063  constrconj  34135  qtophaus  34226  lmdvg  34343  esumcvg  34476  unelldsys  34548  ldgenpisyslem1  34553  eulerpartlemsv3  34751  eulerpartlemgvv  34766  signstfvneq0  34959  reprinfz1  35009  tgoldbachgtd  35049  bnj1185  35181  bnj222  35271  bnj517  35273  bnj1452  35440  bnj1463  35443  derangenlem  35663  subfacp1lem6  35677  subfacp1  35678  resconn  35738  cvmscbv  35750  sat1el2xp  35871  untangtr  36206  dfon2lem3  36275  dfon2lem7  36279  nadddilem2  36713  nadddilem4  36715  nn0prpwlem  36853  neibastop3  36893  fnemeet2  36898  weiunlem  36994  mh-infprim2bi  37078  mh-infprim3bi  37079  fvineqsnf1  38076  fvineqsneu  38077  pibt2  38083  phpreu  38275  poimirlem27  38318  heicant  38326  mblfinlem2  38329  ovoliunnfl  38333  voliunnfl  38335  mbfresfi  38337  upixp  38400  sdclem2  38413  fdc  38416  mettrifi  38428  heiborlem5  38486  heiborlem10  38491  heibor  38492  bfp  38495  disjressuc2  39080  cdleme25cv  41152  cdleme40v  41263  aks4d1p7  42870  aks6d1c1p3  42897  aks6d1c1p4  42898  supinf  43030  fsuppind  43342  mzpclval  43476  dford3lem1  43773  fnwe2lem1  43797  aomclem3  43803  aomclem4  43804  aomclem8  43808  dfac11  43809  hbtlem5  43875  nadd1suc  44139  ntrk2imkb  44783  ntrclsk2  44814  ntrclsk4  44818  fnchoice  45769  cncmpmax  45772  wessf1ornlem  45923  disjinfi  45930  rnmptbdd  45980  rnmptbd2  45984  rnmptbd  45991  supxrunb3  46134  unb2ltle  46149  monoord2xrv  46217  uzubioo2  46303  mccl  46334  climsuse  46344  limsupre  46375  limsuppnf  46445  limsupubuz  46447  limsupmnf  46455  limsupre2  46459  limsupmnfuz  46461  limsupre2mpt  46464  limsupre3  46467  limsupre3mpt  46468  limsupre3uzlem  46469  limsupre3uz  46470  limsupreuz  46471  limsupvaluz2  46472  limsupreuzmpt  46473  climuz  46478  lmbr3  46481  limsupge  46495  liminflelimsup  46510  liminfreuz  46537  xlimpnfxnegmnf  46548  cnrefiisp  46564  xlimmnf  46575  xlimpnf  46576  xlimmnfmpt  46577  xlimpnfmpt  46578  dfxlim2  46582  dvbdfbdioolem2  46663  dvbdfbdioo  46664  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnprodlem3  46682  stoweidlem7  46741  stoweidlem15  46749  stoweidlem35  46769  wallispilem3  46801  fourierdlem68  46908  fourierdlem71  46911  fourierdlem73  46913  fourierdlem87  46927  fourierdlem100  46940  fourierdlem103  46943  fourierdlem104  46944  fourierdlem107  46947  fourierdlem109  46949  fourierdlem112  46952  etransc  47017  qndenserrnbllem  47028  dfsalgen2  47075  subsaliuncl  47092  meaiuninclem  47214  ovnsubaddlem2  47305  hoidmvlelem5  47333  hoidmvle  47334  hoiqssbllem3  47358  vonioo  47416  vonicc  47419  issmf  47462  issmfle  47479  issmfgt  47490  issmfge  47504  smfsuplem2  47546  chnerlem1  47618  2reuimp0  47871  uniimafveqt  48150  sbgoldbm  48569  mogoldbb  48570  bgoldbtbndlem4  48593  bgoldbtbnd  48594  nn0sumshdiglem1  49421  ipolub  49786  ipoglb  49789