Theorem eqimssi 3994

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 3956	. 2 ⊢ 𝐴 ⊆ 𝐴
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtri 3982	1 ⊢ 𝐴 ⊆ 𝐵

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  funi  6569  fpr  7154  tz7.48-2  8434  trcl  9710  zorn2lem4  10504  zmin  12996  elfzo1  13770  om2uzf1oi  14019  0trrel  15056  sumsplit  15856  isumless  15936  rnglidl1  21422  frlmip  21992  ust0  24447  rrxprds  25618  rrxip  25619  ovoliunnul  25736  vitalilem5  25841  logtayl  26895  bdayons  28539  nbgr2vtx1edg  29796  nbuhgr2vtx1edgb  29798  mayetes3i  32196  cycpmconjslem2  33582  esplyind  34072  eulerpartlemsv2  34856  eulerpartlemsv3  34859  eulerpartlemv  34862  eulerpartlemb  34866  poimirlem9  38365  dvasin  38440  dmcoss3  39278  disjALTVid  39590  sticksstones17  43016  sticksstones18  43017  nna4b4nsq  43493  cnvrcl0  44452  corclrcl  44534  trclrelexplem  44538  cotrcltrcl  44552  he0  44611  dvsid  45142  binomcxplemnotnn0  45167  wfaxreg  45810  fourierdlem62  46983  fourierdlem66  46987  isubgr3stgrlem6  48874