Theorem raleqi 3172

Description: Equality inference for restricted universal qualifier. (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 3168	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)

Syntax hints:   ↔ wb 196   = wceq 1523  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946

This theorem is referenced by:  ralrab2  3405  ralprg  4266  raltpg  4268  ralxp  5296  f12dfv  6569  f13dfv  6570  ralrnmpt2  6817  ovmptss  7303  ixpfi2  8305  dffi3  8378  dfoi  8457  fseqenlem1  8885  kmlem12  9021  fzprval  12439  fztpval  12440  hashbc  13275  2prm  15452  prmreclem2  15668  xpsfrnel  16270  xpsle  16288  gsumwspan  17430  sgrp2rid2  17460  psgnunilem3  17962  pmtrsn  17985  ply1coe  19714  cply1coe0bi  19718  islinds2  20200  m2cpminvid2lem  20607  basdif0  20805  ordtbaslem  21040  ptbasfi  21432  ptcnplem  21472  ptrescn  21490  flftg  21847  ust0  22070  minveclem1  23241  minveclem3b  23245  minveclem6  23251  iblcnlem1  23599  ellimc2  23686  ftalem3  24846  dchreq  25028  pntlem3  25343  istrkg2ld  25404  istrkg3ld  25405  lfuhgr1v0e  26191  cplgr0  26377  wlkp1lem8  26633  usgr2pthlem  26715  pthdlem1  26718  pthd  26721  crctcshwlkn0  26769  2wlkdlem4  26893  2wlkdlem5  26894  2pthdlem1  26895  2wlkdlem10  26900  rusgrnumwwlkl1  26935  0ewlk  27092  0wlk  27094  wlk2v2elem2  27134  3wlkdlem4  27140  3wlkdlem5  27141  3pthdlem1  27142  3wlkdlem10  27147  minvecolem1  27858  minvecolem5  27865  minvecolem6  27866  cdj3lem3b  29427  prsiga  30322  hfext  32415  filnetlem4  32501  relowlssretop  33341  relowlpssretop  33342  elghomOLD  33816  iscrngo2  33926  refrelcoss3  34353  tendoset  36364  fnwe2lem2  37938  eliuniincex  39606  eliincex  39607  uzub  39971  liminflelimsuplem  40325  xlimbr  40371  subsaliuncl  40894