Theorem eqimssi 3622

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

Syntax hints:   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  funi  5834  fpr  6326  tz7.48-2  7424  trcl  8487  zorn2lem4  9204  zmin  11660  elfzo1  12385  om2uzf1oi  12614  0trrel  13568  sumsplit  14341  isumless  14416  frlmip  19936  ust0  21833  rrxprds  22985  rrxip  22986  ovoliunnul  23082  vitalilem5  23187  logtayl  24206  mayetes3i  27972  eulerpartlemsv2  29747  eulerpartlemsv3  29750  eulerpartlemv  29753  eulerpartlemb  29757  poimirlem9  32588  dvasin  32666  cnvrcl0  36951  corclrcl  37018  trclrelexplem  37022  cotrcltrcl  37036  he0  37098  idhe  37101  dvsid  37552  binomcxplemnotnn0  37577  fourierdlem62  39061  fourierdlem66  39065  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574