Theorem eqimssi 3959

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

Syntax hints:   = wceq 1543   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  funi  6412  fpr  6969  tz7.48-2  8178  trcl  9344  zorn2lem4  10113  zmin  12540  elfzo1  13292  om2uzf1oi  13526  0trrel  14544  sumsplit  15332  isumless  15409  frlmip  20740  ust0  23117  rrxprds  24286  rrxip  24287  ovoliunnul  24404  vitalilem5  24509  logtayl  25548  nbgr2vtx1edg  27438  nbuhgr2vtx1edgb  27440  mayetes3i  29810  cycpmconjslem2  31141  eulerpartlemsv2  32037  eulerpartlemsv3  32040  eulerpartlemv  32043  eulerpartlemb  32047  poimirlem9  35523  dvasin  35598  dmcoss3  36308  disjALTVid  36600  sticksstones17  39841  sticksstones18  39842  nna4b4nsq  40200  cnvrcl0  40909  corclrcl  40992  trclrelexplem  40996  cotrcltrcl  41010  he0  41069  dvsid  41622  binomcxplemnotnn0  41647  fourierdlem62  43384  fourierdlem66  43388