Theorem eqimssi 4010

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

Syntax hints:   = wceq 1540   ⊆ wss 3917

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  funi  6551  fpr  7129  tz7.48-2  8413  trcl  9688  zorn2lem4  10459  zmin  12910  elfzo1  13680  om2uzf1oi  13925  0trrel  14954  sumsplit  15741  isumless  15818  rnglidl1  21149  frlmip  21694  ust0  24114  rrxprds  25296  rrxip  25297  ovoliunnul  25415  vitalilem5  25520  logtayl  26576  bdayon  28180  nbgr2vtx1edg  29284  nbuhgr2vtx1edgb  29286  mayetes3i  31665  cycpmconjslem2  33119  eulerpartlemsv2  34356  eulerpartlemsv3  34359  eulerpartlemv  34362  eulerpartlemb  34366  poimirlem9  37630  dvasin  37705  dmcoss3  38451  disjALTVid  38754  sticksstones17  42158  sticksstones18  42159  nna4b4nsq  42655  cnvrcl0  43621  corclrcl  43703  trclrelexplem  43707  cotrcltrcl  43721  he0  43780  dvsid  44327  binomcxplemnotnn0  44352  wfaxreg  44997  fourierdlem62  46173  fourierdlem66  46177  isubgr3stgrlem6  47974