Theorem raleqi 3323

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

Syntax hints:   ↔ wb 205   = wceq 1541  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ral 3062  df-rex 3071

This theorem is referenced by:  ralrab2  3691  ralprgf  4690  ralprg  4692  raltpg  4696  ralxp  5834  f12dfv  7256  f13dfv  7257  ralrnmpo  7531  ovmptss  8063  ixpfi2  9335  dffi3  9410  dfoi  9490  ssttrcl  9694  fseqenlem1  10003  kmlem12  10140  fzprval  13546  fztpval  13547  hashbc  14396  2prm  16613  prmreclem2  16834  xpsfrnel  17492  xpsle  17509  gsumwspan  18704  sgrp2rid2  18784  psgnunilem3  19330  pmtrsn  19353  islinds2  21303  ply1coe  21751  cply1coe0bi  21755  m2cpminvid2lem  22187  basdif0  22387  ordtbaslem  22623  ptbasfi  23016  ptcnplem  23056  ptrescn  23074  flftg  23431  ust0  23655  minveclem1  24872  minveclem3b  24876  minveclem6  24882  iblcnlem1  25236  ellimc2  25325  ftalem3  26508  dchreq  26690  pntlem3  27041  negsbdaylem  27459  precsexlem9  27590  istrkg2ld  27640  istrkg3ld  27641  tgcgr4  27711  elntg2  28172  lfuhgr1v0e  28440  cplgr0  28611  wlkp1lem8  28866  usgr2pthlem  28949  pthdlem1  28952  pthd  28955  crctcshwlkn0  29004  2wlkdlem4  29111  2wlkdlem5  29112  2pthdlem1  29113  2wlkdlem10  29118  rusgrnumwwlkl1  29151  0ewlk  29296  0wlk  29298  wlk2v2elem2  29338  3wlkdlem4  29344  3wlkdlem5  29345  3pthdlem1  29346  3wlkdlem10  29351  minvecolem1  30054  minvecolem5  30061  minvecolem6  30062  cdj3lem3b  31620  prsiga  33024  hfext  35049  filnetlem4  35134  relowlssretop  36112  relowlpssretop  36113  elghomOLD  36624  iscrngo2  36734  refrelcoss3  37202  tendoset  39499  fnwe2lem2  41628  nadd1suc  41977  eliuniincex  43633  eliincex  43634  uzub  43978  liminflelimsuplem  44328  xlimbr  44380  subsaliuncl  44911  isomushgr  46330  rrx2pnecoorneor  47113  rrx2linest  47140