Theorem eqimss 3211

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 3172	. 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 3131

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 3137  df-ss 3144

This theorem is referenced by:  eqimss2  3212  uneqin  3388  sssnr  3755  sssnm  3756  ssprr  3758  sstpr  3759  snsspw  3766  pwpwssunieq  3977  elpwuni  3978  disjeq2  3986  disjeq1  3989  pwne  4162  pwssunim  4286  poeq2  4302  seeq1  4341  seeq2  4342  trsucss  4425  onsucelsucr  4509  xp11m  5069  funeq  5238  fnresdm  5327  fssxp  5385  ffdm  5388  fcoi1  5398  fof  5440  dff1o2  5468  fvmptss2  5593  fvmptssdm  5602  fprg  5701  dff1o6  5779  tposeq  6250  el2oss1o  6446  nntri1  6499  nntri2or2  6501  nnsseleq  6504  infnninf  7124  infnninfOLD  7125  nninfwlpoimlemg  7175  exmidontri2or  7244  frec2uzf1od  10408  hashinfuni  10759  setsresg  12502  setsslid  12515  strle1g  12567  cncnpi  13767  hmeores  13854  limcimolemlt  14172  recnprss  14195  0nninf  14792  nninfall  14797