Theorem eqimss2 3248

Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)

Assertion

Ref	Expression
eqimss2	|- ( B = A -> A C_ B )

Proof of Theorem eqimss2

Step	Hyp	Ref	Expression
1		eqimss 3247	. 2 |- ( A = B -> A C_ B )
2	1	eqcoms 2208	1 |- ( B = A -> A C_ B )

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  disjeq2  4025  disjeq1  4028  poeq2  4347  seeq1  4386  seeq2  4387  dmcoeq  4951  xp11m  5121  funeq  5291  fconst3m  5803  tposeq  6333  undifdcss  7020  nninfctlemfo  12361  ennnfonelemk  12771  ennnfonelemss  12781  qnnen  12802  imasaddfnlemg  13146  topgele  14501  topontopn  14509  txdis  14749  edgstruct  15656