Theorem eqimssi 3984

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

Syntax hints:   = wceq 1539   ⊆ wss 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  funi  6495  fpr  7058  tz7.48-2  8304  trcl  9534  zorn2lem4  10305  zmin  12734  elfzo1  13487  om2uzf1oi  13723  0trrel  14741  sumsplit  15529  isumless  15606  frlmip  21034  ust0  23420  rrxprds  24602  rrxip  24603  ovoliunnul  24720  vitalilem5  24825  logtayl  25864  nbgr2vtx1edg  27766  nbuhgr2vtx1edgb  27768  mayetes3i  30140  cycpmconjslem2  31471  eulerpartlemsv2  32374  eulerpartlemsv3  32377  eulerpartlemv  32380  eulerpartlemb  32384  poimirlem9  35834  dvasin  35909  dmcoss3  36667  disjALTVid  36969  sticksstones17  40319  sticksstones18  40320  nna4b4nsq  40692  cnvrcl0  41446  corclrcl  41528  trclrelexplem  41532  cotrcltrcl  41546  he0  41605  dvsid  42162  binomcxplemnotnn0  42187  fourierdlem62  43938  fourierdlem66  43942