Theorem eqimssi 4056

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

Syntax hints:   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

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

This theorem is referenced by:  funi  6600  fpr  7174  tz7.48-2  8481  trcl  9766  zorn2lem4  10537  zmin  12984  elfzo1  13749  om2uzf1oi  13991  0trrel  15017  sumsplit  15801  isumless  15878  rnglidl1  21260  frlmip  21816  ust0  24244  rrxprds  25437  rrxip  25438  ovoliunnul  25556  vitalilem5  25661  logtayl  26717  nbgr2vtx1edg  29382  nbuhgr2vtx1edgb  29384  mayetes3i  31758  cycpmconjslem2  33158  eulerpartlemsv2  34340  eulerpartlemsv3  34343  eulerpartlemv  34346  eulerpartlemb  34350  poimirlem9  37616  dvasin  37691  dmcoss3  38435  disjALTVid  38737  sticksstones17  42145  sticksstones18  42146  nna4b4nsq  42647  cnvrcl0  43615  corclrcl  43697  trclrelexplem  43701  cotrcltrcl  43715  he0  43774  dvsid  44327  binomcxplemnotnn0  44352  fourierdlem62  46124  fourierdlem66  46128  isubgr3stgrlem6  47874