Theorem raleqi 3318

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

Syntax hints:   ↔ wb 208   = wceq 1560  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ral 3077  df-rex 3087

This theorem is referenced by:  ralrab2  3661  ralprgf  4653  ralprg  4655  raltpg  4657  ralxp  5813  f12dfv  7257  f13dfv  7258  ralrnmpo  7535  ovmptss  8072  ixpfi2  9293  dffi3  9377  dfoi  9459  ssttrcl  9670  fseqenlem1  9980  kmlem12  10118  fzprval  13590  fztpval  13591  hashbc  14466  2prm  16726  prmreclem2  16953  xpsfrnel  17592  xpsle  17609  s1chn  18652  chnub  18654  gsumwspan  18880  sgrp2rid2  18963  psgnunilem3  19536  pmtrsn  19559  islinds2  21865  ply1coe  22361  cply1coe0bi  22365  m2cpminvid2lem  22814  basdif0  23013  ordtbaslem  23248  ptbasfi  23641  ptcnplem  23681  ptrescn  23699  flftg  24056  ust0  24280  minveclem1  25486  minveclem3b  25490  minveclem6  25496  iblcnlem1  25850  ellimc2  25939  ftalem3  27139  dchreq  27322  pntlem3  27673  negbdaylem  28149  precsexlem9  28308  0reno  28589  1reno  28590  istrkg2ld  28629  istrkg3ld  28630  tgcgr4  28700  elntg2  29186  lfuhgr1v0e  29455  cplgr0  29626  wlkp1lem8  29879  usgr2pthlem  29963  pthdlem1  29966  pthd  29969  crctcshwlkn0  30021  2wlkdlem4  30128  2wlkdlem5  30129  2pthdlem1  30130  2wlkdlem10  30135  rusgrnumwwlkl1  30171  0ewlk  30316  0wlk  30318  wlk2v2elem2  30358  3wlkdlem4  30364  3wlkdlem5  30365  3pthdlem1  30366  3wlkdlem10  30371  minvecolem1  31077  minvecolem5  31084  minvecolem6  31085  cdj3lem3b  32643  elrgspnsubrunlem2  33429  prsiga  34428  hfext  36533  filnetlem4  36741  mh-infprim2bi  36907  relowlssretop  37857  relowlpssretop  37858  elghomOLD  38386  iscrngo2  38496  refrelcoss3  39052  tendoset  41383  fnwe2lem2  43628  nadd1suc  43969  eliuniincex  45687  eliincex  45688  uzub  46005  liminflelimsuplem  46349  xlimbr  46401  subsaliuncl  46932  gricushgr  48539  isgrlim  48604  rrx2pnecoorneor  49337  rrx2linest  49364