Theorem cbvralvw 3210

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2111  ∀wral 3047

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 2113

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

This theorem is referenced by:  cbvraldva  3212  cbvral2vw  3214  cbvral3vw  3216  cbvral4vw  3217  reu7  3686  cbviinv  4988  disjxun  5087  reusv3i  5340  wereu2  5611  cnvpo  6234  frpomin  6287  f1mpt  7195  dfwe2  7707  tfinds  7790  frrlem1  8216  tfrlem1  8295  tfrlem12  8308  rdglem1  8334  tz7.48lem  8360  cbvixpv  8839  nneneq  9115  marypha1lem  9317  supub  9343  suplub  9344  ordtypecbv  9403  ordtypelem3  9406  ordtypelem9  9412  wemaplem1  9432  brwdom3  9468  ttrclss  9610  ttrclselem2  9616  tcrank  9777  infxpenc2  9913  aceq1  10008  aceq2  10010  dfac5  10020  dfac9  10028  dfac12lem3  10037  kmlem12  10053  kmlem14  10055  cofsmo  10160  infpssrlem4  10197  isfin3ds  10220  isf32lem2  10245  isf32lem11  10254  isf33lem  10257  domtriomlem  10333  axdc3  10345  zorn2lem7  10393  zorn2g  10394  fpwwe2cbv  10521  fpwwecbv  10535  pwfseq  10555  axgroth6  10719  dedekind  11276  suprleub  12088  infregelb  12106  nnsub  12169  uzwo  12809  ublbneg  12831  zsupss  12835  xrub  13211  fsuppmapnn0fiubex  13899  monoord2  13940  faclbnd4lem4  14203  bccl  14229  hashbc  14360  wrdind  14629  wrd2ind  14630  reuccatpfxs1  14654  cau3lem  15262  climmpt2  15480  caucvgrlem  15580  caurcvg2  15585  caucvgb  15587  fsum0diag2  15690  incexclem  15743  cvgrat  15790  mertenslem2  15792  mertens  15793  sqrt2irr  16158  gcdcllem1  16410  lcmfunsnlem1  16548  lcmfunsnlem2lem1  16549  prmind2  16596  prmpwdvds  16816  prmreclem5  16832  prmreclem6  16833  vdwlem7  16899  vdwlem10  16902  vdwlem13  16905  vdwnn  16910  ramcl  16941  isacs2  17559  catpropd  17615  chnind  18527  chnub  18528  grpinvalem  18581  grpinva  18582  gsumvalx  18584  mndind  18736  issubg4  19058  isnsg2  19068  elnmz  19075  gsmsymgreqlem2  19343  psgnunilem5  19406  psgnunilem3  19408  efgsdm  19642  gsummptnn0fzfv  19899  pgpfac1lem5  19993  pgpfac1  19994  pgpfac  19998  ablfaclem3  20001  lbsextg  21099  evlslem2  22014  mpfind  22042  cply1mul  22211  mdetuni0  22536  m2cpminvid2lem  22669  mp2pm2mplem4  22724  chcoeffeqlem  22800  cayhamlem3  22802  elcls3  22998  isclo2  23003  neiptopnei  23047  tgcn  23167  subbascn  23169  txcmplem2  23557  kqfvima  23645  kqt0lem  23651  isr0  23652  r0cld  23653  regr1lem2  23655  fbun  23755  flftg  23911  fclsbas  23936  alexsubALTlem2  23963  alexsubALTlem4  23965  ptcmplem4  23970  tsmsxplem1  24068  tsmsxp  24070  ustuqtop  24161  utopsnneip  24163  prdsxmslem2  24444  isclmp  25024  iscau4  25206  caucfil  25210  iscmet3  25220  bcthlem5  25255  bcth  25256  ovolicc2lem5  25449  uniioombllem6  25516  vitali  25541  ismbf3d  25582  itg1climres  25642  itg2seq  25670  itg2monolem1  25678  itg2mono  25681  rolle  25921  dvlipcn  25926  dvivthlem1  25940  ply1divex  26069  fta1g  26102  dgrco  26208  plydivex  26232  fta1  26243  vieta1  26247  ulmcaulem  26330  ulmcau  26331  abelthlem8  26376  wilth  27008  fta  27017  fsumdvdsmul  27132  dchrelbas3  27176  2sqlem6  27361  2sqlem10  27366  dchrisumlem3  27429  dchrisum  27430  dchrmusumlema  27431  dchrvmasumlema  27438  dchrisum0lema  27452  pntibndlem3  27530  pntlem3  27547  pntleml  27549  pnt3  27550  ostth2lem2  27572  ostth  27577  nosupcbv  27641  nosupdm  27643  nosupbnd1lem4  27650  nosupbnd2  27655  noinfcbv  27656  noinfdm  27658  noinfres  27661  noinfbnd1lem1  27662  noinfbnd2  27670  madebdayim  27833  madebday  27845  cofss  27874  coiniss  27875  precsexlem9  28153  onsfi  28283  n0subs  28289  zs12zodd  28392  zs12bday  28394  axcontlem1  28942  axcontlem6  28947  uspgr2wlkeq  29624  crctcshwlkn0  29799  frgrwopreglem5ALT  30302  grpoideu  30489  ubthlem3  30852  adjsym  31813  lnopunilem1  31990  elunop2  31993  lnophm  31999  cnlnadjlem5  32051  mdbr3  32277  mdbr4  32278  dmdbr3  32285  dmdbr4  32286  mddmd2  32289  fprodex01  32808  prodindf  32844  wrdt2ind  32934  toslublem  32953  tosglblem  32955  archiabl  33167  isarchiofld  33168  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem4  33212  elrgspnsubrunlem2  33215  1arithidom  33502  1arithufdlem3  33511  fedgmul  33644  fldextrspunlsplem  33686  constrconj  33758  qtophaus  33849  lmdvg  33966  esumcvg  34099  unelldsys  34171  ldgenpisyslem1  34176  eulerpartlemsv3  34374  eulerpartlemgvv  34389  signstfvneq0  34585  reprinfz1  34635  tgoldbachgtd  34675  bnj1185  34805  bnj222  34895  bnj517  34897  bnj1452  35064  bnj1463  35067  derangenlem  35215  subfacp1lem6  35229  subfacp1  35230  resconn  35290  cvmscbv  35302  sat1el2xp  35423  untangtr  35758  dfon2lem3  35827  dfon2lem7  35831  nn0prpwlem  36366  neibastop3  36406  fnemeet2  36411  weiunlem2  36507  fvineqsnf1  37454  fvineqsneu  37455  pibt2  37461  phpreu  37654  poimirlem27  37697  heicant  37705  mblfinlem2  37708  ovoliunnfl  37712  voliunnfl  37714  mbfresfi  37716  upixp  37779  sdclem2  37792  fdc  37795  mettrifi  37807  heiborlem5  37865  heiborlem10  37870  heibor  37871  bfp  37874  disjressuc2  38445  cdleme25cv  40467  cdleme40v  40578  aks4d1p7  42186  aks6d1c1p3  42213  aks6d1c1p4  42214  supinf  42345  fsuppind  42693  mzpclval  42828  dford3lem1  43129  fnwe2lem1  43153  aomclem3  43159  aomclem4  43160  aomclem8  43164  dfac11  43165  hbtlem5  43231  nadd1suc  43495  ntrk2imkb  44140  ntrclsk2  44171  ntrclsk4  44175  fnchoice  45136  cncmpmax  45139  wessf1ornlem  45292  disjinfi  45299  rnmptbdd  45352  rnmptbd2  45356  rnmptbd  45363  supxrunb3  45507  unb2ltle  45523  monoord2xrv  45591  uzubioo2  45677  mccl  45708  climsuse  45718  limsupre  45749  limsuppnf  45819  limsupubuz  45821  limsupmnf  45829  limsupre2  45833  limsupmnfuz  45835  limsupre2mpt  45838  limsupre3  45841  limsupre3mpt  45842  limsupre3uzlem  45843  limsupre3uz  45844  limsupreuz  45845  limsupvaluz2  45846  limsupreuzmpt  45847  climuz  45852  lmbr3  45855  limsupge  45869  liminflelimsup  45884  liminfreuz  45911  xlimpnfxnegmnf  45922  cnrefiisp  45938  xlimmnf  45949  xlimpnf  45950  xlimmnfmpt  45951  xlimpnfmpt  45952  dfxlim2  45956  dvbdfbdioolem2  46037  dvbdfbdioo  46038  ioodvbdlimc1lem1  46039  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnprodlem3  46056  stoweidlem7  46115  stoweidlem15  46123  stoweidlem35  46143  wallispilem3  46175  fourierdlem68  46282  fourierdlem71  46285  fourierdlem73  46287  fourierdlem87  46301  fourierdlem100  46314  fourierdlem103  46317  fourierdlem104  46318  fourierdlem107  46321  fourierdlem109  46323  fourierdlem112  46326  etransc  46391  qndenserrnbllem  46402  dfsalgen2  46449  subsaliuncl  46466  meaiuninclem  46588  ovnsubaddlem2  46679  hoidmvlelem5  46707  hoidmvle  46708  hoiqssbllem3  46732  vonioo  46790  vonicc  46793  issmf  46836  issmfle  46853  issmfgt  46864  issmfge  46878  smfsuplem2  46920  chnerlem1  46990  2reuimp0  47224  uniimafveqt  47491  sbgoldbm  47894  mogoldbb  47895  bgoldbtbndlem4  47918  bgoldbtbnd  47919  nn0sumshdiglem1  48732  ipolub  49098  ipoglb  49101