Theorem eqimssi 3996

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

Syntax hints:   = wceq 1542   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  funi  6534  fpr  7111  tz7.48-2  8385  trcl  9651  zorn2lem4  10423  zmin  12871  elfzo1  13642  om2uzf1oi  13890  0trrel  14918  sumsplit  15705  isumless  15782  rnglidl1  21204  frlmip  21750  ust0  24181  rrxprds  25362  rrxip  25363  ovoliunnul  25481  vitalilem5  25586  logtayl  26642  bdayons  28289  nbgr2vtx1edg  29441  nbuhgr2vtx1edgb  29443  mayetes3i  31823  cycpmconjslem2  33255  esplyind  33758  eulerpartlemsv2  34542  eulerpartlemsv3  34545  eulerpartlemv  34548  eulerpartlemb  34552  poimirlem9  37909  dvasin  37984  dmcoss3  38823  disjALTVid  39135  sticksstones17  42562  sticksstones18  42563  nna4b4nsq  43047  cnvrcl0  44010  corclrcl  44092  trclrelexplem  44096  cotrcltrcl  44110  he0  44169  dvsid  44716  binomcxplemnotnn0  44741  wfaxreg  45385  fourierdlem62  46555  fourierdlem66  46559  isubgr3stgrlem6  48360