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 1540   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  funi  6573  fpr  7149  tz7.48-2  8461  trcl  9747  zorn2lem4  10518  zmin  12965  elfzo1  13734  om2uzf1oi  13976  0trrel  15005  sumsplit  15789  isumless  15866  rnglidl1  21198  frlmip  21743  ust0  24163  rrxprds  25346  rrxip  25347  ovoliunnul  25465  vitalilem5  25570  logtayl  26626  bdayon  28230  nbgr2vtx1edg  29334  nbuhgr2vtx1edgb  29336  mayetes3i  31715  cycpmconjslem2  33171  eulerpartlemsv2  34395  eulerpartlemsv3  34398  eulerpartlemv  34401  eulerpartlemb  34405  poimirlem9  37658  dvasin  37733  dmcoss3  38476  disjALTVid  38778  sticksstones17  42181  sticksstones18  42182  nna4b4nsq  42650  cnvrcl0  43616  corclrcl  43698  trclrelexplem  43702  cotrcltrcl  43716  he0  43775  dvsid  44322  binomcxplemnotnn0  44347  wfaxreg  44992  fourierdlem62  46164  fourierdlem66  46168  isubgr3stgrlem6  47950