Theorem eqimss2 3256

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 3255	. 2 |- ( A = B -> A C_ B )
2	1	eqcoms 2210	1 |- ( B = A -> 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:  disjeq2  4039  disjeq1  4042  poeq2  4365  seeq1  4404  seeq2  4405  dmcoeq  4970  xp11m  5140  funeq  5310  fconst3m  5826  tposeq  6356  undifdcss  7046  nninfctlemfo  12476  ennnfonelemk  12886  ennnfonelemss  12896  qnnen  12917  imasaddfnlemg  13261  topgele  14616  topontopn  14624  txdis  14864  edgstruct  15775