Theorem cbvralvw 3215

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ral 3045

This theorem is referenced by:  cbvraldva  3217  cbvral2vw  3219  cbvral3vw  3221  cbvral4vw  3222  reu7  3703  cbviinv  5005  disjxun  5105  reusv3i  5359  wereu2  5635  cnvpo  6260  frpomin  6313  f1mpt  7236  dfwe2  7750  tfinds  7836  frrlem1  8265  tfrlem1  8344  tfrlem12  8357  rdglem1  8383  tz7.48lem  8409  cbvixpv  8888  nneneq  9170  marypha1lem  9384  supub  9410  suplub  9411  ordtypecbv  9470  ordtypelem3  9473  ordtypelem9  9479  wemaplem1  9499  brwdom3  9535  ttrclss  9673  ttrclselem2  9679  tcrank  9837  infxpenc2  9975  aceq1  10070  aceq2  10072  dfac5  10082  dfac9  10090  dfac12lem3  10099  kmlem12  10115  kmlem14  10117  cofsmo  10222  infpssrlem4  10259  isfin3ds  10282  isf32lem2  10307  isf32lem11  10316  isf33lem  10319  domtriomlem  10395  axdc3  10407  zorn2lem7  10455  zorn2g  10456  fpwwe2cbv  10583  fpwwecbv  10597  pwfseq  10617  axgroth6  10781  dedekind  11337  suprleub  12149  infregelb  12167  nnsub  12230  uzwo  12870  ublbneg  12892  zsupss  12896  xrub  13272  fsuppmapnn0fiubex  13957  monoord2  13998  faclbnd4lem4  14261  bccl  14287  hashbc  14418  wrdind  14687  wrd2ind  14688  reuccatpfxs1  14712  cau3lem  15321  climmpt2  15539  caucvgrlem  15639  caurcvg2  15644  caucvgb  15646  fsum0diag2  15749  incexclem  15802  cvgrat  15849  mertenslem2  15851  mertens  15852  sqrt2irr  16217  gcdcllem1  16469  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  prmind2  16655  prmpwdvds  16875  prmreclem5  16891  prmreclem6  16892  vdwlem7  16958  vdwlem10  16961  vdwlem13  16964  vdwnn  16969  ramcl  17000  isacs2  17614  catpropd  17670  grpinvalem  18600  grpinva  18601  gsumvalx  18603  mndind  18755  issubg4  19077  isnsg2  19088  elnmz  19095  gsmsymgreqlem2  19361  psgnunilem5  19424  psgnunilem3  19426  efgsdm  19660  gsummptnn0fzfv  19917  pgpfac1lem5  20011  pgpfac1  20012  pgpfac  20016  ablfaclem3  20019  lbsextg  21072  evlslem2  21986  mpfind  22014  cply1mul  22183  mdetuni0  22508  m2cpminvid2lem  22641  mp2pm2mplem4  22696  chcoeffeqlem  22772  cayhamlem3  22774  elcls3  22970  isclo2  22975  neiptopnei  23019  tgcn  23139  subbascn  23141  txcmplem2  23529  kqfvima  23617  kqt0lem  23623  isr0  23624  r0cld  23625  regr1lem2  23627  fbun  23727  flftg  23883  fclsbas  23908  alexsubALTlem2  23935  alexsubALTlem4  23937  ptcmplem4  23942  tsmsxplem1  24040  tsmsxp  24042  ustuqtop  24134  utopsnneip  24136  prdsxmslem2  24417  isclmp  24997  iscau4  25179  caucfil  25183  iscmet3  25193  bcthlem5  25228  bcth  25229  ovolicc2lem5  25422  uniioombllem6  25489  vitali  25514  ismbf3d  25555  itg1climres  25615  itg2seq  25643  itg2monolem1  25651  itg2mono  25654  rolle  25894  dvlipcn  25899  dvivthlem1  25913  ply1divex  26042  fta1g  26075  dgrco  26181  plydivex  26205  fta1  26216  vieta1  26220  ulmcaulem  26303  ulmcau  26304  abelthlem8  26349  wilth  26981  fta  26990  fsumdvdsmul  27105  dchrelbas3  27149  2sqlem6  27334  2sqlem10  27339  dchrisumlem3  27402  dchrisum  27403  dchrmusumlema  27404  dchrvmasumlema  27411  dchrisum0lema  27425  pntibndlem3  27503  pntlem3  27520  pntleml  27522  pnt3  27523  ostth2lem2  27545  ostth  27550  nosupcbv  27614  nosupdm  27616  nosupbnd1lem4  27623  nosupbnd2  27628  noinfcbv  27629  noinfdm  27631  noinfres  27634  noinfbnd1lem1  27635  noinfbnd2  27643  madebdayim  27799  madebday  27811  cofss  27838  coiniss  27839  precsexlem9  28117  onsfi  28247  n0subs  28253  zs12bday  28343  axcontlem1  28891  axcontlem6  28896  uspgr2wlkeq  29574  crctcshwlkn0  29751  frgrwopreglem5ALT  30251  grpoideu  30438  ubthlem3  30801  adjsym  31762  lnopunilem1  31939  elunop2  31942  lnophm  31948  cnlnadjlem5  32000  mdbr3  32226  mdbr4  32227  dmdbr3  32234  dmdbr4  32235  mddmd2  32238  fprodex01  32750  prodindf  32786  wrdt2ind  32875  toslublem  32898  tosglblem  32900  chnind  32937  chnub  32938  archiabl  33152  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  isarchiofld  33295  1arithidom  33508  1arithufdlem3  33517  fedgmul  33627  fldextrspunlsplem  33668  constrconj  33735  qtophaus  33826  lmdvg  33943  esumcvg  34076  unelldsys  34148  ldgenpisyslem1  34153  eulerpartlemsv3  34352  eulerpartlemgvv  34367  signstfvneq0  34563  reprinfz1  34613  tgoldbachgtd  34653  bnj1185  34783  bnj222  34873  bnj517  34875  bnj1452  35042  bnj1463  35045  derangenlem  35158  subfacp1lem6  35172  subfacp1  35173  resconn  35233  cvmscbv  35245  sat1el2xp  35366  untangtr  35701  dfon2lem3  35773  dfon2lem7  35777  nn0prpwlem  36310  neibastop3  36350  fnemeet2  36355  weiunlem2  36451  fvineqsnf1  37398  fvineqsneu  37399  pibt2  37405  phpreu  37598  poimirlem27  37641  heicant  37649  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  mbfresfi  37660  upixp  37723  sdclem2  37736  fdc  37739  mettrifi  37751  heiborlem5  37809  heiborlem10  37814  heibor  37815  bfp  37818  disjressuc2  38374  cdleme25cv  40352  cdleme40v  40463  aks4d1p7  42071  aks6d1c1p3  42098  aks6d1c1p4  42099  supinf  42230  fsuppind  42578  mzpclval  42713  dford3lem1  43015  fnwe2lem1  43039  aomclem3  43045  aomclem4  43046  aomclem8  43050  dfac11  43051  hbtlem5  43117  nadd1suc  43381  ntrk2imkb  44026  ntrclsk2  44057  ntrclsk4  44061  fnchoice  45023  cncmpmax  45026  wessf1ornlem  45179  disjinfi  45186  rnmptbdd  45239  rnmptbd2  45243  rnmptbd  45250  supxrunb3  45395  unb2ltle  45411  monoord2xrv  45479  uzubioo2  45565  mccl  45596  climsuse  45606  limsupre  45639  limsuppnf  45709  limsupubuz  45711  limsupmnf  45719  limsupre2  45723  limsupmnfuz  45725  limsupre2mpt  45728  limsupre3  45731  limsupre3mpt  45732  limsupre3uzlem  45733  limsupre3uz  45734  limsupreuz  45735  limsupvaluz2  45736  limsupreuzmpt  45737  climuz  45742  lmbr3  45745  limsupge  45759  liminflelimsup  45774  liminfreuz  45801  xlimpnfxnegmnf  45812  cnrefiisp  45828  xlimmnf  45839  xlimpnf  45840  xlimmnfmpt  45841  xlimpnfmpt  45842  dfxlim2  45846  dvbdfbdioolem2  45927  dvbdfbdioo  45928  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem3  45946  stoweidlem7  46005  stoweidlem15  46013  stoweidlem35  46033  wallispilem3  46065  fourierdlem68  46172  fourierdlem71  46175  fourierdlem73  46177  fourierdlem87  46191  fourierdlem100  46204  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem109  46213  fourierdlem112  46216  etransc  46281  qndenserrnbllem  46292  dfsalgen2  46339  subsaliuncl  46356  meaiuninclem  46478  ovnsubaddlem2  46569  hoidmvlelem5  46597  hoidmvle  46598  hoiqssbllem3  46622  vonioo  46680  vonicc  46683  issmf  46726  issmfle  46743  issmfgt  46754  issmfge  46768  smfsuplem2  46810  2reuimp0  47115  uniimafveqt  47382  sbgoldbm  47785  mogoldbb  47786  bgoldbtbndlem4  47809  bgoldbtbnd  47810  nn0sumshdiglem1  48610  ipolub  48976  ipoglb  48979