Theorem eqimssi 3977

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

Syntax hints:   = wceq 1548   ⊆ wss 3885

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 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ss 3902

This theorem is referenced by:  funi  6521  fpr  7101  tz7.48-2  8375  trcl  9644  zorn2lem4  10416  zmin  12889  elfzo1  13662  om2uzf1oi  13910  0trrel  14938  sumsplit  15725  isumless  15805  rnglidl1  21229  frlmip  21757  ust0  24207  rrxprds  25378  rrxip  25379  ovoliunnul  25496  vitalilem5  25601  logtayl  26646  bdayons  28290  nbgr2vtx1edg  29441  nbuhgr2vtx1edgb  29443  mayetes3i  31822  cycpmconjslem2  33240  esplyind  33771  eulerpartlemsv2  34554  eulerpartlemsv3  34557  eulerpartlemv  34560  eulerpartlemb  34564  poimirlem9  38011  dvasin  38086  dmcoss3  38925  disjALTVid  39237  sticksstones17  42663  sticksstones18  42664  nna4b4nsq  43125  cnvrcl0  44084  corclrcl  44166  trclrelexplem  44170  cotrcltrcl  44184  he0  44243  dvsid  44790  binomcxplemnotnn0  44815  wfaxreg  45459  fourierdlem62  46625  fourierdlem66  46629  isubgr3stgrlem6  48476