Theorem eqimssi 3983

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

Syntax hints:   = wceq 1541   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  funi  6462  fpr  7020  tz7.48-2  8257  trcl  9469  zorn2lem4  10239  zmin  12666  elfzo1  13418  om2uzf1oi  13654  0trrel  14673  sumsplit  15461  isumless  15538  frlmip  20966  ust0  23352  rrxprds  24534  rrxip  24535  ovoliunnul  24652  vitalilem5  24757  logtayl  25796  nbgr2vtx1edg  27698  nbuhgr2vtx1edgb  27700  mayetes3i  30070  cycpmconjslem2  31401  eulerpartlemsv2  32304  eulerpartlemsv3  32307  eulerpartlemv  32310  eulerpartlemb  32314  poimirlem9  35765  dvasin  35840  dmcoss3  36550  disjALTVid  36842  sticksstones17  40099  sticksstones18  40100  nna4b4nsq  40477  cnvrcl0  41186  corclrcl  41268  trclrelexplem  41272  cotrcltrcl  41286  he0  41345  dvsid  41902  binomcxplemnotnn0  41927  fourierdlem62  43663  fourierdlem66  43667