Theorem eqimss 3178

Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
eqimss	|- ( A = B -> A C_ B )

Proof of Theorem eqimss

Step	Hyp	Ref	Expression
1		eqss 3139	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2	1	simplbi 272	1 |- ( A = B -> A C_ B )

Syntax hints:   -> wi 4   = wceq 1332   C_ wss 3098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-11 1483  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-in 3104  df-ss 3111

This theorem is referenced by:  eqimss2  3179  uneqin  3354  sssnr  3712  sssnm  3713  ssprr  3715  sstpr  3716  snsspw  3723  pwpwssunieq  3933  elpwuni  3934  disjeq2  3942  disjeq1  3945  pwne  4116  pwssunim  4239  poeq2  4255  seeq1  4294  seeq2  4295  trsucss  4378  onsucelsucr  4461  xp11m  5017  funeq  5183  fnresdm  5272  fssxp  5330  ffdm  5333  fcoi1  5343  fof  5385  dff1o2  5412  fvmptss2  5536  fvmptssdm  5545  fprg  5643  dff1o6  5717  tposeq  6184  nntri1  6432  nntri2or2  6434  nnsseleq  6437  infnninf  7052  infnninfOLD  7053  exmidontri2or  7157  frec2uzf1od  10283  hashinfuni  10628  setsresg  12167  setsslid  12179  strle1g  12219  cncnpi  12567  hmeores  12654  limcimolemlt  12972  recnprss  12995  el2oss1o  13503  0nninf  13515  nninfall  13522