Theorem eqimssi 3993

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

Syntax hints:   = wceq 1542   ⊆ wss 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-ss 3917

This theorem is referenced by:  funi  6523  fpr  7099  tz7.48-2  8373  trcl  9639  zorn2lem4  10411  zmin  12859  elfzo1  13630  om2uzf1oi  13878  0trrel  14906  sumsplit  15693  isumless  15770  rnglidl1  21189  frlmip  21735  ust0  24166  rrxprds  25347  rrxip  25348  ovoliunnul  25466  vitalilem5  25571  logtayl  26627  bdayon  28255  nbgr2vtx1edg  29404  nbuhgr2vtx1edgb  29406  mayetes3i  31785  cycpmconjslem2  33216  esplyind  33710  eulerpartlemsv2  34494  eulerpartlemsv3  34497  eulerpartlemv  34500  eulerpartlemb  34504  poimirlem9  37799  dvasin  37874  dmcoss3  38713  disjALTVid  39025  sticksstones17  42452  sticksstones18  42453  nna4b4nsq  42940  cnvrcl0  43903  corclrcl  43985  trclrelexplem  43989  cotrcltrcl  44003  he0  44062  dvsid  44609  binomcxplemnotnn0  44634  wfaxreg  45278  fourierdlem62  46449  fourierdlem66  46453  isubgr3stgrlem6  48254