Theorem cbvralvw 3234

Description: Change the bound variable of a restricted universal quantifier using implicit substitution. Version of cbvralv 3361 with a disjoint variable condition, which does not require ax-10 2138, ax-11 2154, ax-12 2174, 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 2821	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvralvw.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2032	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3059	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3059	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1534   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ral 3059

This theorem is referenced by:  cbvraldva  3236  cbvral2vw  3238  cbvral3vw  3240  cbvral4vw  3241  reu7  3740  cbviinv  5045  disjxun  5145  reusv3i  5409  wereu2  5685  cnvpo  6308  frpomin  6362  f1mpt  7280  dfwe2  7792  tfinds  7880  frrlem1  8309  wfrlem1OLD  8346  tfrlem1  8414  tfrlem12  8427  rdglem1  8453  tz7.48lem  8479  cbvixpv  8953  nneneq  9243  nneneqOLD  9255  marypha1lem  9470  supub  9496  suplub  9497  ordtypecbv  9554  ordtypelem3  9557  ordtypelem9  9563  wemaplem1  9583  brwdom3  9619  ttrclss  9757  ttrclselem2  9763  tcrank  9921  infxpenc2  10059  aceq1  10154  aceq2  10156  dfac5  10166  dfac9  10174  dfac12lem3  10183  kmlem12  10199  kmlem14  10201  cofsmo  10306  infpssrlem4  10343  isfin3ds  10366  isf32lem2  10391  isf32lem11  10400  isf33lem  10403  domtriomlem  10479  axdc3  10491  zorn2lem7  10539  zorn2g  10540  fpwwe2cbv  10667  fpwwecbv  10681  pwfseq  10701  axgroth6  10865  dedekind  11421  suprleub  12231  infregelb  12249  nnsub  12307  uzwo  12950  ublbneg  12972  zsupss  12976  xrub  13350  fsuppmapnn0fiubex  14029  monoord2  14070  faclbnd4lem4  14331  bccl  14357  hashbc  14488  wrdind  14756  wrd2ind  14757  reuccatpfxs1  14781  cau3lem  15389  climmpt2  15605  caucvgrlem  15705  caurcvg2  15710  caucvgb  15712  fsum0diag2  15815  incexclem  15868  cvgrat  15915  mertenslem2  15917  mertens  15918  sqrt2irr  16281  gcdcllem1  16532  lcmfunsnlem1  16670  lcmfunsnlem2lem1  16671  prmind2  16718  prmpwdvds  16937  prmreclem5  16953  prmreclem6  16954  vdwlem7  17020  vdwlem10  17023  vdwlem13  17026  vdwnn  17031  ramcl  17062  isacs2  17697  catpropd  17753  grpinvalem  18698  grpinva  18699  gsumvalx  18701  mndind  18853  issubg4  19175  isnsg2  19186  elnmz  19193  gsmsymgreqlem2  19463  psgnunilem5  19526  psgnunilem3  19528  efgsdm  19762  gsummptnn0fzfv  20019  pgpfac1lem5  20113  pgpfac1  20114  pgpfac  20118  ablfaclem3  20121  lbsextg  21181  evlslem2  22120  mpfind  22148  cply1mul  22315  mdetuni0  22642  m2cpminvid2lem  22775  mp2pm2mplem4  22830  chcoeffeqlem  22906  cayhamlem3  22908  elcls3  23106  isclo2  23111  neiptopnei  23155  tgcn  23275  subbascn  23277  txcmplem2  23665  kqfvima  23753  kqt0lem  23759  isr0  23760  r0cld  23761  regr1lem2  23763  fbun  23863  flftg  24019  fclsbas  24044  alexsubALTlem2  24071  alexsubALTlem4  24073  ptcmplem4  24078  tsmsxplem1  24176  tsmsxp  24178  ustuqtop  24270  utopsnneip  24272  prdsxmslem2  24557  isclmp  25143  iscau4  25326  caucfil  25330  iscmet3  25340  bcthlem5  25375  bcth  25376  ovolicc2lem5  25569  uniioombllem6  25636  vitali  25661  ismbf3d  25702  itg1climres  25763  itg2seq  25791  itg2monolem1  25799  itg2mono  25802  rolle  26042  dvlipcn  26047  dvivthlem1  26061  ply1divex  26190  fta1g  26223  dgrco  26329  plydivex  26353  fta1  26364  vieta1  26368  ulmcaulem  26451  ulmcau  26452  abelthlem8  26497  wilth  27128  fta  27137  fsumdvdsmul  27252  dchrelbas3  27296  2sqlem6  27481  2sqlem10  27486  dchrisumlem3  27549  dchrisum  27550  dchrmusumlema  27551  dchrvmasumlema  27558  dchrisum0lema  27572  pntibndlem3  27650  pntlem3  27667  pntleml  27669  pnt3  27670  ostth2lem2  27692  ostth  27697  nosupcbv  27761  nosupdm  27763  nosupbnd1lem4  27770  nosupbnd2  27775  noinfcbv  27776  noinfdm  27778  noinfres  27781  noinfbnd1lem1  27782  noinfbnd2  27790  madebdayim  27940  madebday  27952  cofss  27978  coiniss  27979  precsexlem9  28253  n0subs  28374  zs12bday  28438  axcontlem1  28993  axcontlem6  28998  uspgr2wlkeq  29678  crctcshwlkn0  29850  frgrwopreglem5ALT  30350  grpoideu  30537  ubthlem3  30900  adjsym  31861  lnopunilem1  32038  elunop2  32041  lnophm  32047  cnlnadjlem5  32099  mdbr3  32325  mdbr4  32326  dmdbr3  32333  dmdbr4  32334  mddmd2  32337  fprodex01  32831  wrdt2ind  32922  toslublem  32946  tosglblem  32948  chnind  32984  chnub  32985  archiabl  33187  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  isarchiofld  33326  1arithidom  33544  1arithufdlem3  33553  fedgmul  33658  constrconj  33749  qtophaus  33796  lmdvg  33913  prodindf  34003  esumcvg  34066  unelldsys  34138  ldgenpisyslem1  34143  eulerpartlemsv3  34342  eulerpartlemgvv  34357  signstfvneq0  34565  reprinfz1  34615  tgoldbachgtd  34655  bnj1185  34785  bnj222  34875  bnj517  34877  bnj1452  35044  bnj1463  35047  derangenlem  35155  subfacp1lem6  35169  subfacp1  35170  resconn  35230  cvmscbv  35242  sat1el2xp  35363  untangtr  35693  dfon2lem3  35766  dfon2lem7  35770  nn0prpwlem  36304  neibastop3  36344  fnemeet2  36349  weiunlem2  36445  fvineqsnf1  37392  fvineqsneu  37393  pibt2  37399  phpreu  37590  poimirlem27  37633  heicant  37641  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  mbfresfi  37652  upixp  37715  sdclem2  37728  fdc  37731  mettrifi  37743  heiborlem5  37801  heiborlem10  37806  heibor  37807  bfp  37810  disjressuc2  38369  cdleme25cv  40340  cdleme40v  40451  aks4d1p7  42064  aks6d1c1p3  42091  aks6d1c1p4  42092  supinf  42261  fsuppind  42576  mzpclval  42712  dford3lem1  43014  fnwe2lem1  43038  aomclem3  43044  aomclem4  43045  aomclem8  43049  dfac11  43050  hbtlem5  43116  nadd1suc  43381  ntrk2imkb  44026  ntrclsk2  44057  ntrclsk4  44061  fnchoice  44966  cncmpmax  44969  wessf1ornlem  45127  disjinfi  45134  rnmptbdd  45189  rnmptbd2  45193  rnmptbd  45200  supxrunb3  45348  unb2ltle  45364  monoord2xrv  45433  uzubioo2  45521  mccl  45553  climsuse  45563  limsupre  45596  limsuppnf  45666  limsupubuz  45668  limsupmnf  45676  limsupre2  45680  limsupmnfuz  45682  limsupre2mpt  45685  limsupre3  45688  limsupre3mpt  45689  limsupre3uzlem  45690  limsupre3uz  45691  limsupreuz  45692  limsupvaluz2  45693  limsupreuzmpt  45694  climuz  45699  lmbr3  45702  limsupge  45716  liminflelimsup  45731  liminfreuz  45758  xlimpnfxnegmnf  45769  cnrefiisp  45785  xlimmnf  45796  xlimpnf  45797  xlimmnfmpt  45798  xlimpnfmpt  45799  dfxlim2  45803  dvbdfbdioolem2  45884  dvbdfbdioo  45885  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem3  45903  stoweidlem7  45962  stoweidlem15  45970  stoweidlem35  45990  wallispilem3  46022  fourierdlem68  46129  fourierdlem71  46132  fourierdlem73  46134  fourierdlem87  46148  fourierdlem100  46161  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  fourierdlem109  46170  fourierdlem112  46173  etransc  46238  qndenserrnbllem  46249  dfsalgen2  46296  subsaliuncl  46313  meaiuninclem  46435  ovnsubaddlem2  46526  hoidmvlelem5  46554  hoidmvle  46555  hoiqssbllem3  46579  vonioo  46637  vonicc  46640  issmf  46683  issmfle  46700  issmfgt  46711  issmfge  46725  smfsuplem2  46767  2reuimp0  47063  uniimafveqt  47305  sbgoldbm  47708  mogoldbb  47709  bgoldbtbndlem4  47732  bgoldbtbnd  47733  nn0sumshdiglem1  48470  ipolub  48776  ipoglb  48779