Theorem cbvralvw 3211

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  ∀wral 3048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2808  df-ral 3049

This theorem is referenced by:  cbvraldva  3213  cbvral2vw  3215  cbvral3vw  3217  cbvral4vw  3218  reu7  3687  cbviinv  4990  disjxun  5091  reusv3i  5344  wereu2  5616  cnvpo  6239  frpomin  6292  f1mpt  7201  dfwe2  7713  tfinds  7796  frrlem1  8222  tfrlem1  8301  tfrlem12  8314  rdglem1  8340  tz7.48lem  8366  cbvixpv  8845  nneneq  9122  marypha1lem  9324  supub  9350  suplub  9351  ordtypecbv  9410  ordtypelem3  9413  ordtypelem9  9419  wemaplem1  9439  brwdom3  9475  ttrclss  9617  ttrclselem2  9623  tcrank  9784  infxpenc2  9920  aceq1  10015  aceq2  10017  dfac5  10027  dfac9  10035  dfac12lem3  10044  kmlem12  10060  kmlem14  10062  cofsmo  10167  infpssrlem4  10204  isfin3ds  10227  isf32lem2  10252  isf32lem11  10261  isf33lem  10264  domtriomlem  10340  axdc3  10352  zorn2lem7  10400  zorn2g  10401  fpwwe2cbv  10528  fpwwecbv  10542  pwfseq  10562  axgroth6  10726  dedekind  11283  suprleub  12095  infregelb  12113  nnsub  12176  uzwo  12811  ublbneg  12833  zsupss  12837  xrub  13213  fsuppmapnn0fiubex  13901  monoord2  13942  faclbnd4lem4  14205  bccl  14231  hashbc  14362  wrdind  14631  wrd2ind  14632  reuccatpfxs1  14656  cau3lem  15264  climmpt2  15482  caucvgrlem  15582  caurcvg2  15587  caucvgb  15589  fsum0diag2  15692  incexclem  15745  cvgrat  15792  mertenslem2  15794  mertens  15795  sqrt2irr  16160  gcdcllem1  16412  lcmfunsnlem1  16550  lcmfunsnlem2lem1  16551  prmind2  16598  prmpwdvds  16818  prmreclem5  16834  prmreclem6  16835  vdwlem7  16901  vdwlem10  16904  vdwlem13  16907  vdwnn  16912  ramcl  16943  isacs2  17561  catpropd  17617  chnind  18529  chnub  18530  grpinvalem  18583  grpinva  18584  gsumvalx  18586  mndind  18738  issubg4  19060  isnsg2  19070  elnmz  19077  gsmsymgreqlem2  19345  psgnunilem5  19408  psgnunilem3  19410  efgsdm  19644  gsummptnn0fzfv  19901  pgpfac1lem5  19995  pgpfac1  19996  pgpfac  20000  ablfaclem3  20003  lbsextg  21101  evlslem2  22015  mpfind  22043  cply1mul  22212  mdetuni0  22537  m2cpminvid2lem  22670  mp2pm2mplem4  22725  chcoeffeqlem  22801  cayhamlem3  22803  elcls3  22999  isclo2  23004  neiptopnei  23048  tgcn  23168  subbascn  23170  txcmplem2  23558  kqfvima  23646  kqt0lem  23652  isr0  23653  r0cld  23654  regr1lem2  23656  fbun  23756  flftg  23912  fclsbas  23937  alexsubALTlem2  23964  alexsubALTlem4  23966  ptcmplem4  23971  tsmsxplem1  24069  tsmsxp  24071  ustuqtop  24162  utopsnneip  24164  prdsxmslem2  24445  isclmp  25025  iscau4  25207  caucfil  25211  iscmet3  25221  bcthlem5  25256  bcth  25257  ovolicc2lem5  25450  uniioombllem6  25517  vitali  25542  ismbf3d  25583  itg1climres  25643  itg2seq  25671  itg2monolem1  25679  itg2mono  25682  rolle  25922  dvlipcn  25927  dvivthlem1  25941  ply1divex  26070  fta1g  26103  dgrco  26209  plydivex  26233  fta1  26244  vieta1  26248  ulmcaulem  26331  ulmcau  26332  abelthlem8  26377  wilth  27009  fta  27018  fsumdvdsmul  27133  dchrelbas3  27177  2sqlem6  27362  2sqlem10  27367  dchrisumlem3  27430  dchrisum  27431  dchrmusumlema  27432  dchrvmasumlema  27439  dchrisum0lema  27453  pntibndlem3  27531  pntlem3  27548  pntleml  27550  pnt3  27551  ostth2lem2  27573  ostth  27578  nosupcbv  27642  nosupdm  27644  nosupbnd1lem4  27651  nosupbnd2  27656  noinfcbv  27657  noinfdm  27659  noinfres  27662  noinfbnd1lem1  27663  noinfbnd2  27671  madebdayim  27834  madebday  27846  cofss  27875  coiniss  27876  precsexlem9  28154  onsfi  28284  n0subs  28290  zs12zodd  28393  zs12bday  28395  axcontlem1  28944  axcontlem6  28949  uspgr2wlkeq  29626  crctcshwlkn0  29801  frgrwopreglem5ALT  30304  grpoideu  30491  ubthlem3  30854  adjsym  31815  lnopunilem1  31992  elunop2  31995  lnophm  32001  cnlnadjlem5  32053  mdbr3  32279  mdbr4  32280  dmdbr3  32287  dmdbr4  32288  mddmd2  32291  fprodex01  32813  prodindf  32851  wrdt2ind  32941  toslublem  32960  tosglblem  32962  archiabl  33174  isarchiofld  33175  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  elrgspnsubrunlem2  33222  1arithidom  33509  1arithufdlem3  33518  fedgmul  33665  fldextrspunlsplem  33707  constrconj  33779  qtophaus  33870  lmdvg  33987  esumcvg  34120  unelldsys  34192  ldgenpisyslem1  34197  eulerpartlemsv3  34395  eulerpartlemgvv  34410  signstfvneq0  34606  reprinfz1  34656  tgoldbachgtd  34696  bnj1185  34826  bnj222  34916  bnj517  34918  bnj1452  35085  bnj1463  35088  derangenlem  35236  subfacp1lem6  35250  subfacp1  35251  resconn  35311  cvmscbv  35323  sat1el2xp  35444  untangtr  35779  dfon2lem3  35848  dfon2lem7  35852  nn0prpwlem  36387  neibastop3  36427  fnemeet2  36432  weiunlem2  36528  fvineqsnf1  37475  fvineqsneu  37476  pibt2  37482  phpreu  37664  poimirlem27  37707  heicant  37715  mblfinlem2  37718  ovoliunnfl  37722  voliunnfl  37724  mbfresfi  37726  upixp  37789  sdclem2  37802  fdc  37805  mettrifi  37817  heiborlem5  37875  heiborlem10  37880  heibor  37881  bfp  37884  disjressuc2  38455  cdleme25cv  40477  cdleme40v  40588  aks4d1p7  42196  aks6d1c1p3  42223  aks6d1c1p4  42224  supinf  42360  fsuppind  42708  mzpclval  42842  dford3lem1  43143  fnwe2lem1  43167  aomclem3  43173  aomclem4  43174  aomclem8  43178  dfac11  43179  hbtlem5  43245  nadd1suc  43509  ntrk2imkb  44154  ntrclsk2  44185  ntrclsk4  44189  fnchoice  45150  cncmpmax  45153  wessf1ornlem  45306  disjinfi  45313  rnmptbdd  45366  rnmptbd2  45370  rnmptbd  45377  supxrunb3  45521  unb2ltle  45537  monoord2xrv  45605  uzubioo2  45691  mccl  45722  climsuse  45732  limsupre  45763  limsuppnf  45833  limsupubuz  45835  limsupmnf  45843  limsupre2  45847  limsupmnfuz  45849  limsupre2mpt  45852  limsupre3  45855  limsupre3mpt  45856  limsupre3uzlem  45857  limsupre3uz  45858  limsupreuz  45859  limsupvaluz2  45860  limsupreuzmpt  45861  climuz  45866  lmbr3  45869  limsupge  45883  liminflelimsup  45898  liminfreuz  45925  xlimpnfxnegmnf  45936  cnrefiisp  45952  xlimmnf  45963  xlimpnf  45964  xlimmnfmpt  45965  xlimpnfmpt  45966  dfxlim2  45970  dvbdfbdioolem2  46051  dvbdfbdioo  46052  ioodvbdlimc1lem1  46053  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvnprodlem3  46070  stoweidlem7  46129  stoweidlem15  46137  stoweidlem35  46157  wallispilem3  46189  fourierdlem68  46296  fourierdlem71  46299  fourierdlem73  46301  fourierdlem87  46315  fourierdlem100  46328  fourierdlem103  46331  fourierdlem104  46332  fourierdlem107  46335  fourierdlem109  46337  fourierdlem112  46340  etransc  46405  qndenserrnbllem  46416  dfsalgen2  46463  subsaliuncl  46480  meaiuninclem  46602  ovnsubaddlem2  46693  hoidmvlelem5  46721  hoidmvle  46722  hoiqssbllem3  46746  vonioo  46804  vonicc  46807  issmf  46850  issmfle  46867  issmfgt  46878  issmfge  46892  smfsuplem2  46934  chnerlem1  47004  2reuimp0  47238  uniimafveqt  47505  sbgoldbm  47908  mogoldbb  47909  bgoldbtbndlem4  47932  bgoldbtbnd  47933  nn0sumshdiglem1  48746  ipolub  49112  ipoglb  49115