Theorem eqimss2 3658

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 3657	. 2 |- ( A = B -> A C_ B )
2	1	eqcoms 2630	1 |- ( B = A -> A C_ B )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  ifpprsnss  4299  disjeq2  4624  disjeq1  4627  poeq2  5039  freq2  5085  seeq1  5086  seeq2  5087  dmcoeq  5388  xp11  5569  suc11  5831  funeq  5908  fconst3  6477  sorpssuni  6946  sorpssint  6947  tposeq  7354  oaass  7641  odi  7659  oen0  7666  inficl  8331  cantnfp1lem1  8575  cantnflem1  8586  fodomfi2  8883  zorng  9326  rlimclim  14277  imasaddfnlem  16188  imasvscafn  16197  gasubg  17735  pgpssslw  18029  dprddisj2  18438  dprd2da  18441  evlslem6  19513  topgele  20734  topontopn  20744  toponmre  20897  connima  21228  islocfin  21320  ptbasfi  21384  txdis  21435  neifil  21684  elfm3  21754  rnelfmlem  21756  alexsubALTlem3  21853  alexsubALTlem4  21854  utopsnneiplem  22051  lmclimf  23102  uniiccdif  23346  dv11cn  23764  plypf1  23968  2pthon3v  26839  hstoh  29091  dmdi2  29163  disjeq1f  29387  eulerpartlemd  30428  rrvdmss  30511  refssfne  32353  neibastop3  32357  topmeet  32359  topjoin  32360  fnemeet2  32362  fnejoin1  32363  bj-restuni  33050  heiborlem3  33612  lsatelbN  34293  lkrscss  34385  lshpset2N  34406  mapdrvallem2  36934  hdmaprnlem3eN  37150  hdmaplkr  37205  uneqsn  38321  ssrecnpr  38507  founiiun  39360  founiiun0  39377  caragendifcl  40728