Theorem eqimss 3234

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

Syntax hints:   -> wi 4   = wceq 1364   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  eqimss2  3235  uneqin  3411  sssnr  3780  sssnm  3781  ssprr  3783  sstpr  3784  snsspw  3791  pwpwssunieq  4002  elpwuni  4003  disjeq2  4011  disjeq1  4014  pwne  4190  pwssunim  4316  poeq2  4332  seeq1  4371  seeq2  4372  trsucss  4455  onsucelsucr  4541  xp11m  5105  funeq  5275  fnresdm  5364  fssxp  5422  ffdm  5425  fcoi1  5435  fof  5477  dff1o2  5506  fvmptss2  5633  fvmptssdm  5643  fprg  5742  dff1o6  5820  tposeq  6302  el2oss1o  6498  nntri1  6551  nntri2or2  6553  nnsseleq  6556  infnninf  7185  infnninfOLD  7186  nninfwlpoimlemg  7236  exmidontri2or  7305  frec2uzf1od  10480  hashinfuni  10851  setsresg  12659  setsslid  12672  strle1g  12727  cncnpi  14407  hmeores  14494  limcimolemlt  14843  recnprss  14866  0nninf  15564  nninfall  15569