Theorem eqimssi 3996

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

Syntax hints:   = wceq 1540   ⊆ wss 3903

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-ss 3920

This theorem is referenced by:  funi  6514  fpr  7088  tz7.48-2  8364  trcl  9624  zorn2lem4  10393  zmin  12845  elfzo1  13615  om2uzf1oi  13860  0trrel  14888  sumsplit  15675  isumless  15752  rnglidl1  21139  frlmip  21685  ust0  24105  rrxprds  25287  rrxip  25288  ovoliunnul  25406  vitalilem5  25511  logtayl  26567  bdayon  28180  nbgr2vtx1edg  29299  nbuhgr2vtx1edgb  29301  mayetes3i  31677  cycpmconjslem2  33106  eulerpartlemsv2  34342  eulerpartlemsv3  34345  eulerpartlemv  34348  eulerpartlemb  34352  poimirlem9  37629  dvasin  37704  dmcoss3  38450  disjALTVid  38753  sticksstones17  42156  sticksstones18  42157  nna4b4nsq  42653  cnvrcl0  43618  corclrcl  43700  trclrelexplem  43704  cotrcltrcl  43718  he0  43777  dvsid  44324  binomcxplemnotnn0  44349  wfaxreg  44994  fourierdlem62  46169  fourierdlem66  46173  isubgr3stgrlem6  47975