Theorem eqimss 3151

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 3112	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2	1	simplbi 272	1 |- ( A = B -> A C_ B )

Syntax hints:   -> wi 4   = wceq 1331   C_ wss 3071

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  eqimss2  3152  uneqin  3327  sssnr  3680  sssnm  3681  ssprr  3683  sstpr  3684  snsspw  3691  pwpwssunieq  3901  elpwuni  3902  disjeq2  3910  disjeq1  3913  pwne  4084  pwssunim  4206  poeq2  4222  seeq1  4261  seeq2  4262  trsucss  4345  onsucelsucr  4424  xp11m  4977  funeq  5143  fnresdm  5232  fssxp  5290  ffdm  5293  fcoi1  5303  fof  5345  dff1o2  5372  fvmptss2  5496  fvmptssdm  5505  fprg  5603  dff1o6  5677  tposeq  6144  nntri1  6392  nntri2or2  6394  nnsseleq  6397  infnninf  7022  frec2uzf1od  10179  hashinfuni  10523  setsresg  11997  setsslid  12009  strle1g  12049  cncnpi  12397  hmeores  12484  limcimolemlt  12802  recnprss  12825  el2oss1o  13188  0nninf  13197  nninfall  13204