Theorem eqimssi 3990

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

Syntax hints:   = wceq 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  funi  6513  fpr  7087  tz7.48-2  8361  trcl  9618  zorn2lem4  10390  zmin  12842  elfzo1  13612  om2uzf1oi  13860  0trrel  14888  sumsplit  15675  isumless  15752  rnglidl1  21169  frlmip  21715  ust0  24135  rrxprds  25316  rrxip  25317  ovoliunnul  25435  vitalilem5  25540  logtayl  26596  bdayon  28209  nbgr2vtx1edg  29328  nbuhgr2vtx1edgb  29330  mayetes3i  31709  cycpmconjslem2  33124  eulerpartlemsv2  34371  eulerpartlemsv3  34374  eulerpartlemv  34377  eulerpartlemb  34381  poimirlem9  37668  dvasin  37743  dmcoss3  38554  disjALTVid  38852  sticksstones17  42255  sticksstones18  42256  nna4b4nsq  42752  cnvrcl0  43717  corclrcl  43799  trclrelexplem  43803  cotrcltrcl  43817  he0  43876  dvsid  44423  binomcxplemnotnn0  44448  wfaxreg  45092  fourierdlem62  46265  fourierdlem66  46269  isubgr3stgrlem6  48070