Theorem eqimssi 3993

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

Syntax hints:   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-in 3908  df-ss 3918

This theorem is referenced by:  funi  6520  fpr  7086  tz7.48-2  8347  trcl  9589  zorn2lem4  10360  zmin  12789  elfzo1  13542  om2uzf1oi  13778  0trrel  14791  sumsplit  15579  isumless  15656  frlmip  21090  ust0  23476  rrxprds  24658  rrxip  24659  ovoliunnul  24776  vitalilem5  24881  logtayl  25920  nbgr2vtx1edg  28005  nbuhgr2vtx1edgb  28007  mayetes3i  30378  cycpmconjslem2  31707  eulerpartlemsv2  32623  eulerpartlemsv3  32626  eulerpartlemv  32629  eulerpartlemb  32633  poimirlem9  35942  dvasin  36017  dmcoss3  36771  disjALTVid  37073  sticksstones17  40427  sticksstones18  40428  nna4b4nsq  40810  cnvrcl0  41606  corclrcl  41688  trclrelexplem  41692  cotrcltrcl  41706  he0  41765  dvsid  42322  binomcxplemnotnn0  42347  fourierdlem62  44097  fourierdlem66  44101