Theorem raleqi 3321

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

Syntax hints:   ↔ wb 209   = wceq 1563  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ral 3080  df-rex 3090

This theorem is referenced by:  ralrab2  3664  ralprgf  4656  ralprg  4658  raltpg  4660  ralxp  5818  f12dfv  7261  f13dfv  7262  ralrnmpo  7539  ovmptss  8076  ixpfi2  9295  dffi3  9379  dfoi  9461  ssttrcl  9672  fseqenlem1  9996  kmlem12  10133  fzprval  13604  fztpval  13605  hashbc  14480  2prm  16740  prmreclem2  16967  xpsfrnel  17606  xpsle  17623  s1chn  18666  chnub  18668  gsumwspan  18895  sgrp2rid2  18978  psgnunilem3  19557  pmtrsn  19580  islinds2  21923  ply1coe  22419  cply1coe0bi  22423  m2cpminvid2lem  22872  basdif0  23071  ordtbaslem  23306  ptbasfi  23699  ptcnplem  23739  ptrescn  23757  flftg  24114  ust0  24338  minveclem1  25544  minveclem3b  25548  minveclem6  25554  iblcnlem1  25908  ellimc2  25997  ftalem3  27197  dchreq  27380  pntlem3  27731  negbdaylem  28207  precsexlem9  28366  0reno  28647  1reno  28648  istrkg2ld  28687  istrkg3ld  28688  tgcgr4  28758  elntg2  29244  lfuhgr1v0e  29513  cplgr0  29684  wlkp1lem8  29937  usgr2pthlem  30021  pthdlem1  30024  pthd  30027  crctcshwlkn0  30079  2wlkdlem4  30186  2wlkdlem5  30187  2pthdlem1  30188  2wlkdlem10  30193  rusgrnumwwlkl1  30229  0ewlk  30374  0wlk  30376  wlk2v2elem2  30416  3wlkdlem4  30422  3wlkdlem5  30423  3pthdlem1  30424  3wlkdlem10  30429  minvecolem1  31135  minvecolem5  31142  minvecolem6  31143  cdj3lem3b  32701  elrgspnsubrunlem2  33481  prsiga  34438  hfext  36546  filnetlem4  36754  mh-infprim2bi  36920  relowlssretop  37869  relowlpssretop  37870  elghomOLD  38398  iscrngo2  38508  refrelcoss3  39064  tendoset  41395  fnwe2lem2  43640  nadd1suc  43981  eliuniincex  45685  eliincex  45686  uzub  46003  liminflelimsuplem  46347  xlimbr  46399  subsaliuncl  46930  gricushgr  48537  isgrlim  48602  rrx2pnecoorneor  49346  rrx2linest  49373