Theorem eqimss 3201

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

Syntax hints:   -> wi 4   = wceq 1348   C_ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqimss2  3202  uneqin  3378  sssnr  3740  sssnm  3741  ssprr  3743  sstpr  3744  snsspw  3751  pwpwssunieq  3961  elpwuni  3962  disjeq2  3970  disjeq1  3973  pwne  4146  pwssunim  4269  poeq2  4285  seeq1  4324  seeq2  4325  trsucss  4408  onsucelsucr  4492  xp11m  5049  funeq  5218  fnresdm  5307  fssxp  5365  ffdm  5368  fcoi1  5378  fof  5420  dff1o2  5447  fvmptss2  5571  fvmptssdm  5580  fprg  5679  dff1o6  5755  tposeq  6226  el2oss1o  6422  nntri1  6475  nntri2or2  6477  nnsseleq  6480  infnninf  7100  infnninfOLD  7101  nninfwlpoimlemg  7151  exmidontri2or  7220  frec2uzf1od  10362  hashinfuni  10711  setsresg  12454  setsslid  12466  strle1g  12508  cncnpi  13022  hmeores  13109  limcimolemlt  13427  recnprss  13450  0nninf  14037  nninfall  14042