Theorem eqimssi 4024

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

Syntax hints:   = wceq 1539   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3948

This theorem is referenced by:  funi  6578  fpr  7154  tz7.48-2  8464  trcl  9750  zorn2lem4  10521  zmin  12968  elfzo1  13734  om2uzf1oi  13976  0trrel  15002  sumsplit  15786  isumless  15863  rnglidl1  21204  frlmip  21752  ust0  24174  rrxprds  25359  rrxip  25360  ovoliunnul  25478  vitalilem5  25583  logtayl  26638  nbgr2vtx1edg  29295  nbuhgr2vtx1edgb  29297  mayetes3i  31676  cycpmconjslem2  33114  eulerpartlemsv2  34319  eulerpartlemsv3  34322  eulerpartlemv  34325  eulerpartlemb  34329  poimirlem9  37595  dvasin  37670  dmcoss3  38413  disjALTVid  38715  sticksstones17  42123  sticksstones18  42124  nna4b4nsq  42633  cnvrcl0  43600  corclrcl  43682  trclrelexplem  43686  cotrcltrcl  43700  he0  43759  dvsid  44307  binomcxplemnotnn0  44332  wfaxreg  44974  fourierdlem62  46140  fourierdlem66  46144  isubgr3stgrlem6  47896