Theorem eqimssi 3983

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

Syntax hints:   = wceq 1542   ⊆ wss 3890

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 3907

This theorem is referenced by:  funi  6526  fpr  7103  tz7.48-2  8376  trcl  9644  zorn2lem4  10416  zmin  12889  elfzo1  13662  om2uzf1oi  13910  0trrel  14938  sumsplit  15725  isumless  15805  rnglidl1  21226  frlmip  21772  ust0  24199  rrxprds  25370  rrxip  25371  ovoliunnul  25488  vitalilem5  25593  logtayl  26641  bdayons  28286  nbgr2vtx1edg  29437  nbuhgr2vtx1edgb  29439  mayetes3i  31819  cycpmconjslem2  33235  esplyind  33738  eulerpartlemsv2  34522  eulerpartlemsv3  34525  eulerpartlemv  34528  eulerpartlemb  34532  poimirlem9  37970  dvasin  38045  dmcoss3  38884  disjALTVid  39196  sticksstones17  42622  sticksstones18  42623  nna4b4nsq  43113  cnvrcl0  44076  corclrcl  44158  trclrelexplem  44162  cotrcltrcl  44176  he0  44235  dvsid  44782  binomcxplemnotnn0  44807  wfaxreg  45451  fourierdlem62  46620  fourierdlem66  46624  isubgr3stgrlem6  48465