Theorem eqimssi 4007

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

Syntax hints:   = wceq 1540   ⊆ wss 3914

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 3931

This theorem is referenced by:  funi  6548  fpr  7126  tz7.48-2  8410  trcl  9681  zorn2lem4  10452  zmin  12903  elfzo1  13673  om2uzf1oi  13918  0trrel  14947  sumsplit  15734  isumless  15811  rnglidl1  21142  frlmip  21687  ust0  24107  rrxprds  25289  rrxip  25290  ovoliunnul  25408  vitalilem5  25513  logtayl  26569  bdayon  28173  nbgr2vtx1edg  29277  nbuhgr2vtx1edgb  29279  mayetes3i  31658  cycpmconjslem2  33112  eulerpartlemsv2  34349  eulerpartlemsv3  34352  eulerpartlemv  34355  eulerpartlemb  34359  poimirlem9  37623  dvasin  37698  dmcoss3  38444  disjALTVid  38747  sticksstones17  42151  sticksstones18  42152  nna4b4nsq  42648  cnvrcl0  43614  corclrcl  43696  trclrelexplem  43700  cotrcltrcl  43714  he0  43773  dvsid  44320  binomcxplemnotnn0  44345  wfaxreg  44990  fourierdlem62  46166  fourierdlem66  46170  isubgr3stgrlem6  47970