Theorem eqimssi 3557

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 3522	. 2
2		eqimssi.1	. 2
3	1, 2	sseqtri 3535	1

Syntax hints:  =wceq 1395  C_wss 3475

This theorem is referenced by:  funi  5623  fpr  6079  tz7.48-2  7126  trcl  8180  zorn2lem4  8900  zmin  11207  elfzo1  11871  om2uzf1oi  12064  sumsplit  13583  isumless  13657  frlmip  18809  ust0  20722  rrxprds  21821  rrxip  21822  ovoliunnul  21918  vitalilem5  22021  logtayl  23041  mayetes3i  26648  eulerpartlemsv2  28297  eulerpartlemsv3  28300  eulerpartlemv  28303  eulerpartlemb  28307  dvasin  30103  dvsid  31236  binomcxplemnotnn0  31261  fourierdlem62  31951  fourierdlem66  31955  0trrel  37776  he0  37807  idhe  37810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489