Theorem eqimss 3209

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

Syntax hints:   -> wi 4   = wceq 1353   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  eqimss2  3210  uneqin  3386  sssnr  3753  sssnm  3754  ssprr  3756  sstpr  3757  snsspw  3764  pwpwssunieq  3975  elpwuni  3976  disjeq2  3984  disjeq1  3987  pwne  4160  pwssunim  4284  poeq2  4300  seeq1  4339  seeq2  4340  trsucss  4423  onsucelsucr  4507  xp11m  5067  funeq  5236  fnresdm  5325  fssxp  5383  ffdm  5386  fcoi1  5396  fof  5438  dff1o2  5466  fvmptss2  5591  fvmptssdm  5600  fprg  5699  dff1o6  5776  tposeq  6247  el2oss1o  6443  nntri1  6496  nntri2or2  6498  nnsseleq  6501  infnninf  7121  infnninfOLD  7122  nninfwlpoimlemg  7172  exmidontri2or  7241  frec2uzf1od  10405  hashinfuni  10756  setsresg  12499  setsslid  12512  strle1g  12564  cncnpi  13698  hmeores  13785  limcimolemlt  14103  recnprss  14126  0nninf  14723  nninfall  14728