Theorem eqimssi 4004

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

Syntax hints:   = wceq 1540   ⊆ wss 3911

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 3928

This theorem is referenced by:  funi  6532  fpr  7108  tz7.48-2  8387  trcl  9657  zorn2lem4  10428  zmin  12879  elfzo1  13649  om2uzf1oi  13894  0trrel  14923  sumsplit  15710  isumless  15787  rnglidl1  21174  frlmip  21720  ust0  24140  rrxprds  25322  rrxip  25323  ovoliunnul  25441  vitalilem5  25546  logtayl  26602  bdayon  28213  nbgr2vtx1edg  29330  nbuhgr2vtx1edgb  29332  mayetes3i  31708  cycpmconjslem2  33127  eulerpartlemsv2  34342  eulerpartlemsv3  34345  eulerpartlemv  34348  eulerpartlemb  34352  poimirlem9  37616  dvasin  37691  dmcoss3  38437  disjALTVid  38740  sticksstones17  42144  sticksstones18  42145  nna4b4nsq  42641  cnvrcl0  43607  corclrcl  43689  trclrelexplem  43693  cotrcltrcl  43707  he0  43766  dvsid  44313  binomcxplemnotnn0  44338  wfaxreg  44983  fourierdlem62  46159  fourierdlem66  46163  isubgr3stgrlem6  47963