Theorem eqimssi 3998

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

Syntax hints:   = wceq 1562   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-ss 3923

This theorem is referenced by:  funi  6555  fpr  7139  tz7.48-2  8415  trcl  9685  zorn2lem4  10458  zmin  12947  elfzo1  13720  om2uzf1oi  13968  0trrel  14996  sumsplit  15797  isumless  15877  rnglidl1  21304  frlmip  21832  ust0  24282  rrxprds  25453  rrxip  25454  ovoliunnul  25571  vitalilem5  25676  logtayl  26727  bdayons  28371  nbgr2vtx1edg  29553  nbuhgr2vtx1edgb  29555  mayetes3i  31934  cycpmconjslem2  33337  esplyind  33874  eulerpartlemsv2  34657  eulerpartlemsv3  34660  eulerpartlemv  34663  eulerpartlemb  34667  poimirlem9  38133  dvasin  38208  dmcoss3  39047  disjALTVid  39359  sticksstones17  42785  sticksstones18  42786  nna4b4nsq  43247  cnvrcl0  44206  corclrcl  44288  trclrelexplem  44292  cotrcltrcl  44306  he0  44365  dvsid  44912  binomcxplemnotnn0  44937  wfaxreg  45581  fourierdlem62  46747  fourierdlem66  46751  isubgr3stgrlem6  48598