Theorem eqimss 3255

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

Syntax hints:   -> wi 4   = wceq 1373   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  eqimss2  3256  uneqin  3432  ssprsseq  3806  sssnr  3807  sssnm  3808  ssprr  3810  sstpr  3811  snsspw  3818  pwpwssunieq  4030  elpwuni  4031  disjeq2  4039  disjeq1  4042  pwne  4220  pwssunim  4349  poeq2  4365  seeq1  4404  seeq2  4405  trsucss  4488  onsucelsucr  4574  xp11m  5140  funeq  5310  fnresdm  5404  fssxp  5463  ffdm  5466  fcoi1  5478  fof  5520  dff1o2  5549  fvmptss2  5677  fvmptssdm  5687  fprg  5790  dff1o6  5868  tposeq  6356  el2oss1o  6552  nntri1  6605  nntri2or2  6607  nnsseleq  6610  infnninf  7252  infnninfOLD  7253  nninfwlpoimlemg  7303  exmidontri2or  7389  frec2uzf1od  10588  hashinfuni  10959  setsresg  12985  setsslid  12998  strle1g  13053  cncnpi  14815  hmeores  14902  limcimolemlt  15251  recnprss  15274  plycoeid3  15344  0nninf  16143  nninfall  16148