Theorem eqimssi 4003

Description: Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)

Hypothesis

Ref	Expression
eqimssi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqimssi	⊢ 𝐴 ⊆ 𝐵

Proof of Theorem eqimssi

Step	Hyp	Ref	Expression
1		ssid 3965	. 2 ⊢ 𝐴 ⊆ 𝐴
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtri 3991	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   = wceq 1567   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3928

This theorem is referenced by:  funi  6569  fpr  7152  tz7.48-2  8429  trcl  9697  zorn2lem4  10483  zmin  12968  elfzo1  13741  om2uzf1oi  13989  0trrel  15018  sumsplit  15819  isumless  15899  rnglidl1  21336  frlmip  21897  ust0  24346  rrxprds  25517  rrxip  25518  ovoliunnul  25635  vitalilem5  25740  logtayl  26791  bdayons  28435  nbgr2vtx1edg  29641  nbuhgr2vtx1edgb  29643  mayetes3i  32022  cycpmconjslem2  33416  esplyind  33910  eulerpartlemsv2  34693  eulerpartlemsv3  34696  eulerpartlemv  34699  eulerpartlemb  34703  poimirlem9  38203  dvasin  38278  dmcoss3  39117  disjALTVid  39429  sticksstones17  42855  sticksstones18  42856  nna4b4nsq  43319  cnvrcl0  44278  corclrcl  44360  trclrelexplem  44364  cotrcltrcl  44378  he0  44437  dvsid  44968  binomcxplemnotnn0  44993  wfaxreg  45636  fourierdlem62  46809  fourierdlem66  46813  isubgr3stgrlem6  48660