Theorem cbvralvw 3235

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 2155, ax-12 2172, ax-13 2372. (Contributed by NM, 28-Jan-1997.) Avoid ax-13 2372. (Revised by Gino Giotto, 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 345	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
4	3	cbvalvw 2040	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
5		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
6		df-ral 3063	. 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓))
7	4, 5, 6	3bitr4i 303	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1540   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811  df-ral 3063

This theorem is referenced by:  cbvraldva  3237  cbvral2vw  3239  cbvral3vw  3241  cbvral4vw  3242  reu7  3728  disjxun  5146  reusv3i  5402  wereu2  5673  cnvpo  6284  frpomin  6339  f1mpt  7257  dfwe2  7758  tfinds  7846  frrlem1  8268  wfrlem1OLD  8305  tfrlem1  8373  tfrlem12  8386  rdglem1  8412  tz7.48lem  8438  nneneq  9206  nneneqOLD  9218  marypha1lem  9425  supub  9451  suplub  9452  ordtypecbv  9509  ordtypelem3  9512  ordtypelem9  9518  wemaplem1  9538  brwdom3  9574  ttrclss  9712  ttrclselem2  9718  tcrank  9876  infxpenc2  10014  aceq1  10109  aceq2  10111  dfac5  10120  dfac9  10128  dfac12lem3  10137  kmlem12  10153  kmlem14  10155  cofsmo  10261  infpssrlem4  10298  isfin3ds  10321  isf32lem2  10346  isf32lem11  10355  isf33lem  10358  domtriomlem  10434  axdc3  10446  zorn2lem7  10494  zorn2g  10495  fpwwe2cbv  10622  fpwwecbv  10636  pwfseq  10656  axgroth6  10820  dedekind  11374  suprleub  12177  infregelb  12195  nnsub  12253  uzwo  12892  ublbneg  12914  zsupss  12918  xrub  13288  fsuppmapnn0fiubex  13954  monoord2  13996  faclbnd4lem4  14253  bccl  14279  hashbc  14409  wrdind  14669  wrd2ind  14670  reuccatpfxs1  14694  cau3lem  15298  climmpt2  15514  caucvgrlem  15616  caurcvg2  15621  caucvgb  15623  fsum0diag2  15726  incexclem  15779  cvgrat  15826  mertenslem2  15828  mertens  15829  sqrt2irr  16189  gcdcllem1  16437  lcmfunsnlem1  16571  lcmfunsnlem2lem1  16572  prmind2  16619  prmpwdvds  16834  prmreclem5  16850  prmreclem6  16851  vdwlem7  16917  vdwlem10  16920  vdwlem13  16923  vdwnn  16928  ramcl  16959  isacs2  17594  catpropd  17650  grprinvlem  18589  grpinva  18590  gsumvalx  18592  mndind  18706  issubg4  19020  isnsg2  19031  elnmz  19038  gsmsymgreqlem2  19294  psgnunilem5  19357  psgnunilem3  19359  efgsdm  19593  gsummptnn0fzfv  19850  pgpfac1lem5  19944  pgpfac1  19945  pgpfac  19949  ablfaclem3  19952  lbsextg  20768  evlslem2  21634  mpfind  21662  cply1mul  21810  mdetuni0  22115  m2cpminvid2lem  22248  mp2pm2mplem4  22303  chcoeffeqlem  22379  cayhamlem3  22381  elcls3  22579  isclo2  22584  neiptopnei  22628  tgcn  22748  subbascn  22750  txcmplem2  23138  kqfvima  23226  kqt0lem  23232  isr0  23233  r0cld  23234  regr1lem2  23236  fbun  23336  flftg  23492  fclsbas  23517  alexsubALTlem2  23544  alexsubALTlem4  23546  ptcmplem4  23551  tsmsxplem1  23649  tsmsxp  23651  ustuqtop  23743  utopsnneip  23745  prdsxmslem2  24030  isclmp  24605  iscau4  24788  caucfil  24792  iscmet3  24802  bcthlem5  24837  bcth  24838  ovolicc2lem5  25030  uniioombllem6  25097  vitali  25122  ismbf3d  25163  itg1climres  25224  itg2seq  25252  itg2monolem1  25260  itg2mono  25263  rolle  25499  dvlipcn  25503  dvivthlem1  25517  ply1divex  25646  fta1g  25677  dgrco  25781  plydivex  25802  fta1  25813  vieta1  25817  ulmcaulem  25898  ulmcau  25899  abelthlem8  25943  wilth  26565  fta  26574  dchrelbas3  26731  2sqlem6  26916  2sqlem10  26921  dchrisumlem3  26984  dchrisum  26985  dchrmusumlema  26986  dchrvmasumlema  26993  dchrisum0lema  27007  pntibndlem3  27085  pntlem3  27102  pntleml  27104  pnt3  27105  ostth2lem2  27127  ostth  27132  nosupcbv  27195  nosupdm  27197  nosupbnd1lem4  27204  nosupbnd2  27209  noinfcbv  27210  noinfdm  27212  noinfres  27215  noinfbnd1lem1  27216  noinfbnd2  27224  madebdayim  27372  madebday  27384  cofss  27407  coiniss  27408  precsexlem9  27651  axcontlem1  28212  axcontlem6  28217  uspgr2wlkeq  28893  crctcshwlkn0  29065  frgrwopreglem5ALT  29565  grpoideu  29750  ubthlem3  30113  adjsym  31074  lnopunilem1  31251  elunop2  31254  lnophm  31260  cnlnadjlem5  31312  mdbr3  31538  mdbr4  31539  dmdbr3  31546  dmdbr4  31547  mddmd2  31550  fprodex01  32019  wrdt2ind  32105  toslublem  32130  tosglblem  32132  archiabl  32332  isarchiofld  32424  fedgmul  32705  qtophaus  32805  lmdvg  32922  prodindf  33010  esumcvg  33073  unelldsys  33145  ldgenpisyslem1  33150  eulerpartlemsv3  33349  eulerpartlemgvv  33364  signstfvneq0  33572  reprinfz1  33623  tgoldbachgtd  33663  bnj1185  33793  bnj222  33883  bnj517  33885  bnj1452  34052  bnj1463  34055  derangenlem  34151  subfacp1lem6  34165  subfacp1  34166  resconn  34226  cvmscbv  34238  sat1el2xp  34359  untangtr  34672  dfon2lem3  34746  dfon2lem7  34750  nn0prpwlem  35196  neibastop3  35236  fnemeet2  35241  fvineqsnf1  36280  fvineqsneu  36281  pibt2  36287  phpreu  36461  poimirlem27  36504  heicant  36512  mblfinlem2  36515  ovoliunnfl  36519  voliunnfl  36521  mbfresfi  36523  upixp  36586  sdclem2  36599  fdc  36602  mettrifi  36614  heiborlem5  36672  heiborlem10  36677  heibor  36678  bfp  36681  disjressuc2  37247  cdleme25cv  39218  cdleme40v  39329  aks4d1p7  40937  fsuppind  41160  mzpclval  41449  dford3lem1  41751  fnwe2lem1  41778  aomclem3  41784  aomclem4  41785  aomclem8  41789  dfac11  41790  hbtlem5  41856  nadd1suc  42128  ntrk2imkb  42774  ntrclsk2  42805  ntrclsk4  42809  fnchoice  43699  cncmpmax  43702  wessf1ornlem  43868  disjinfi  43877  rnmptbdd  43935  rnmptbd2  43940  rnmptbd  43947  supxrunb3  44096  unb2ltle  44112  monoord2xrv  44181  uzubioo2  44269  mccl  44301  climsuse  44311  limsupre  44344  limsuppnf  44414  limsupubuz  44416  limsupmnf  44424  limsupre2  44428  limsupmnfuz  44430  limsupre2mpt  44433  limsupre3  44436  limsupre3mpt  44437  limsupre3uzlem  44438  limsupre3uz  44439  limsupreuz  44440  limsupvaluz2  44441  limsupreuzmpt  44442  climuz  44447  lmbr3  44450  limsupge  44464  liminflelimsup  44479  liminfreuz  44506  xlimpnfxnegmnf  44517  cnrefiisp  44533  xlimmnf  44544  xlimpnf  44545  xlimmnfmpt  44546  xlimpnfmpt  44547  dfxlim2  44551  dvbdfbdioolem2  44632  dvbdfbdioo  44633  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnprodlem3  44651  stoweidlem7  44710  stoweidlem15  44718  stoweidlem35  44738  wallispilem3  44770  fourierdlem68  44877  fourierdlem71  44880  fourierdlem73  44882  fourierdlem87  44896  fourierdlem100  44909  fourierdlem103  44912  fourierdlem104  44913  fourierdlem107  44916  fourierdlem109  44918  fourierdlem112  44921  etransc  44986  qndenserrnbllem  44997  dfsalgen2  45044  subsaliuncl  45061  meaiuninclem  45183  ovnsubaddlem2  45274  hoidmvlelem5  45302  hoidmvle  45303  hoiqssbllem3  45327  vonioo  45385  vonicc  45388  issmf  45431  issmfle  45448  issmfgt  45459  issmfge  45473  smfsuplem2  45515  2reuimp0  45809  uniimafveqt  46036  sbgoldbm  46439  mogoldbb  46440  bgoldbtbndlem4  46463  bgoldbtbnd  46464  nn0sumshdiglem1  47261  ipolub  47567  ipoglb  47570