Theorem raleqi 3321

Description: Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
raleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
raleqi	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleqi

Step	Hyp	Ref	Expression
1		raleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		raleq 3320	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ral 3081  df-rex 3091

This theorem is used by:  ralrab2  3659  ralprgf  4656  ralprg  4658  raltpg  4660  ralxp  5828  f12dfv  7312  f13dfv  7313  ralrnmpo  7591  ovmptssOLD  8140  fnwe2lem3  8184  ixpfi2  9377  dffi3  9460  dfoi  9542  ssttrcl  9753  fseqenlem1  10142  kmlem12  10279  fzprval  13759  fztpval  13760  hashbc  14639  2prm  16911  prmreclem2  17139  xpsfrnel  17784  xpsle  17801  s1chn  18844  chnub  18846  gsumwspan  19092  sgrp2rid2  19175  psgnunilem3  19761  pmtrsn  19784  islinds2  22174  ply1coe  22671  cply1coe0bi  22675  m2cpminvid2lem  23127  basdif0  23326  ordtbaslem  23561  ptbasfi  23955  ptcnplem  23995  ptrescn  24013  flftg  24370  ust0  24594  minveclem1  25800  minveclem3b  25804  minveclem6  25810  iblcnlem1  26163  ellimc2  26252  ftalem3  27459  dchreq  27642  pntlem3  27993  negbdaylem  28499  precsexlem9  28658  0reno  28939  1reno  28940  istrkg2ld  28979  istrkg3ld  28980  tgcgr4  29051  elntg2  29620  lfuhgr1v0e  29892  cplgr0  30063  wlkp1lem8  30316  usgr2pthlem  30406  pthdlem1  30409  pthd  30412  crctcshwlkn0  30467  2wlkdlem4  30574  2wlkdlem5  30575  2pthdlem1  30576  2wlkdlem10  30581  rusgrnumwwlkl1  30617  0ewlk  30762  0wlk  30764  wlk2v2elem2  30814  3wlkdlem4  30820  3wlkdlem5  30821  3pthdlem1  30822  3wlkdlem10  30827  minvecolem1  31533  minvecolem5  31540  minvecolem6  31541  cdj3lem3b  33099  elrgspnsubrunlem2  33908  prsiga  34874  hfext  37149  nmulrid  37161  filnetlem4  37384  mh-infprim2bi  37550  relowlssretop  38554  relowlpssretop  38555  elghomOLD  39087  iscrngo2  39197  refrelcoss3  39751  tendoset  42082  nadd1suc  44655  eliuniincex  46397  eliincex  46398  uzub  46714  liminflelimsuplem  47058  xlimbr  47110  subsaliuncl  47641  gricushgr  49288  isgrlim  49353  rrx2pnecoorneor  50159  rrx2linest  50185