Theorem eqimssi 3659

Description: Infer subclass relationship from equality. (Contributed by NM, 6-Jan-2007.)

Hypothesis

Ref	Expression
eqimssi.1	|- A = B

Assertion

Ref	Expression
eqimssi	|- A C_ B

Proof of Theorem eqimssi

Step	Hyp	Ref	Expression
1		ssid 3624	. 2 |- A C_ A
2		eqimssi.1	. 2 |- A = B
3	1, 2	sseqtri 3637	1 |- A C_ B

Syntax hints:   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  funi  5920  fpr  6421  tz7.48-2  7537  trcl  8604  zorn2lem4  9321  zmin  11784  elfzo1  12517  om2uzf1oi  12752  0trrel  13720  sumsplit  14499  isumless  14577  frlmip  20117  ust0  22023  rrxprds  23177  rrxip  23178  ovoliunnul  23275  vitalilem5  23381  logtayl  24406  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  mayetes3i  28588  eulerpartlemsv2  30420  eulerpartlemsv3  30423  eulerpartlemv  30426  eulerpartlemb  30430  poimirlem9  33418  dvasin  33496  cnvrcl0  37932  corclrcl  37999  trclrelexplem  38003  cotrcltrcl  38017  he0  38078  idhe  38081  dvsid  38530  binomcxplemnotnn0  38555  fourierdlem62  40385  fourierdlem66  40389