Theorem raleqi 3358

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 3354	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

Syntax hints:   ↔ wb 205   = wceq 1539  ∀wral 3062

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-ral 3063

This theorem is referenced by:  ralrab2  3640  ralprgf  4632  ralprg  4634  raltpg  4638  ralxp  5763  f12dfv  7177  f13dfv  7178  ralrnmpo  7444  ovmptss  7965  ixpfi2  9161  dffi3  9234  dfoi  9314  ssttrcl  9517  fseqenlem1  9826  kmlem12  9963  fzprval  13363  fztpval  13364  hashbc  14210  2prm  16442  prmreclem2  16663  xpsfrnel  17318  xpsle  17335  gsumwspan  18530  sgrp2rid2  18610  psgnunilem3  19149  pmtrsn  19172  islinds2  21065  ply1coe  21512  cply1coe0bi  21516  m2cpminvid2lem  21948  basdif0  22148  ordtbaslem  22384  ptbasfi  22777  ptcnplem  22817  ptrescn  22835  flftg  23192  ust0  23416  minveclem1  24633  minveclem3b  24637  minveclem6  24643  iblcnlem1  24997  ellimc2  25086  ftalem3  26269  dchreq  26451  pntlem3  26802  istrkg2ld  26866  istrkg3ld  26867  tgcgr4  26937  elntg2  27398  lfuhgr1v0e  27666  cplgr0  27837  wlkp1lem8  28093  usgr2pthlem  28176  pthdlem1  28179  pthd  28182  crctcshwlkn0  28231  2wlkdlem4  28338  2wlkdlem5  28339  2pthdlem1  28340  2wlkdlem10  28345  rusgrnumwwlkl1  28378  0ewlk  28523  0wlk  28525  wlk2v2elem2  28565  3wlkdlem4  28571  3wlkdlem5  28572  3pthdlem1  28573  3wlkdlem10  28578  minvecolem1  29281  minvecolem5  29288  minvecolem6  29289  cdj3lem3b  30847  prsiga  32144  hfext  34530  filnetlem4  34615  relowlssretop  35578  relowlpssretop  35579  elghomOLD  36089  iscrngo2  36199  refrelcoss3  36623  tendoset  38815  fnwe2lem2  40914  eliuniincex  42697  eliincex  42698  uzub  43019  liminflelimsuplem  43365  xlimbr  43417  subsaliuncl  43946  isomushgr  45336  rrx2pnecoorneor  46119  rrx2linest  46146