Theorem raleqi 3294

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

Syntax hints:   ↔ wb 206   = wceq 1540  ∀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-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  ralrab2  3666  ralprgf  4654  ralprg  4656  raltpg  4658  ralxp  5795  f12dfv  7230  f13dfv  7231  ralrnmpo  7508  ovmptss  8049  ixpfi2  9277  dffi3  9358  dfoi  9440  ssttrcl  9644  fseqenlem1  9953  kmlem12  10091  fzprval  13522  fztpval  13523  hashbc  14394  2prm  16638  prmreclem2  16864  xpsfrnel  17501  xpsle  17518  gsumwspan  18755  sgrp2rid2  18835  psgnunilem3  19410  pmtrsn  19433  islinds2  21755  ply1coe  22218  cply1coe0bi  22222  m2cpminvid2lem  22674  basdif0  22873  ordtbaslem  23108  ptbasfi  23501  ptcnplem  23541  ptrescn  23559  flftg  23916  ust0  24140  minveclem1  25357  minveclem3b  25361  minveclem6  25367  iblcnlem1  25722  ellimc2  25811  ftalem3  27018  dchreq  27202  pntlem3  27553  negsbdaylem  28002  precsexlem9  28157  istrkg2ld  28440  istrkg3ld  28441  tgcgr4  28511  elntg2  28965  lfuhgr1v0e  29234  cplgr0  29405  wlkp1lem8  29659  usgr2pthlem  29743  pthdlem1  29746  pthd  29749  crctcshwlkn0  29801  2wlkdlem4  29908  2wlkdlem5  29909  2pthdlem1  29910  2wlkdlem10  29915  rusgrnumwwlkl1  29948  0ewlk  30093  0wlk  30095  wlk2v2elem2  30135  3wlkdlem4  30141  3wlkdlem5  30142  3pthdlem1  30143  3wlkdlem10  30148  minvecolem1  30853  minvecolem5  30860  minvecolem6  30861  cdj3lem3b  32419  s1chn  32982  chnub  32984  elrgspnsubrunlem2  33215  prsiga  34114  hfext  36164  filnetlem4  36362  relowlssretop  37344  relowlpssretop  37345  elghomOLD  37874  iscrngo2  37984  refrelcoss3  38447  tendoset  40746  fnwe2lem2  43033  nadd1suc  43374  eliuniincex  45096  eliincex  45097  uzub  45420  liminflelimsuplem  45766  xlimbr  45818  subsaliuncl  46349  gricushgr  47910  isgrlim  47974  rrx2pnecoorneor  48697  rrx2linest  48724