Theorem eqimss 3278

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

Syntax hints:   -> wi 4   = wceq 1395   C_ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqimss2  3279  uneqin  3455  ssprsseq  3830  sssnr  3831  sssnm  3832  ssprr  3834  sstpr  3835  snsspw  3842  pwpwssunieq  4054  elpwuni  4055  disjeq2  4063  disjeq1  4066  pwne  4244  pwssunim  4375  poeq2  4391  seeq1  4430  seeq2  4431  trsucss  4514  onsucelsucr  4600  xp11m  5167  funeq  5338  fnresdm  5432  fssxp  5491  ffdm  5494  fcoi1  5506  fof  5548  dff1o2  5577  fvmptss2  5709  fvmptssdm  5719  fprg  5822  dff1o6  5900  tposeq  6393  el2oss1o  6589  nntri1  6642  nntri2or2  6644  nnsseleq  6647  infnninf  7291  infnninfOLD  7292  nninfwlpoimlemg  7342  exmidontri2or  7428  frec2uzf1od  10628  hashinfuni  10999  setsresg  13070  setsslid  13083  strle1g  13139  cncnpi  14902  hmeores  14989  limcimolemlt  15338  recnprss  15361  plycoeid3  15431  0nninf  16370  nninfall  16375