Theorem eqimss2 3409

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

Syntax hints:   -> wi 4   = wceq 1369   C_ wss 3328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3335  df-ss 3342

This theorem is referenced by:  disjeq2  4266  disjeq1  4269  poeq2  4645  freq2  4691  seeq1  4692  seeq2  4693  suc11  4822  dmcoeq  5102  xp11  5273  funeq  5437  fconst3  5941  sorpssuni  6369  sorpssint  6370  tposeq  6747  oaass  7000  odi  7018  oen0  7025  inficl  7675  cantnfp1lem1  7886  cantnflem1  7897  cantnfp1lem1OLD  7912  cantnfp1lem3OLD  7914  cantnflem1dOLD  7919  cantnflem1OLD  7920  fodomfi2  8230  zorng  8673  rlimclim  13024  imasaddfnlem  14466  imasvscafn  14475  gasubg  15820  pgpssslw  16113  dprddisj2  16537  dprddisj2OLD  16538  dprd2da  16541  evlslem6  17598  evlslem6OLD  17599  topgele  18539  topontopn  18547  toponmre  18697  conima  19029  ptbasfi  19154  txdis  19205  neifil  19453  elfm3  19523  rnelfmlem  19525  alexsubALTlem3  19621  alexsubALTlem4  19622  utopsnneiplem  19822  lmclimf  20814  uniiccdif  21058  dv11cn  21473  plypf1  21680  subgores  23791  hstoh  25636  dmdi2  25708  eulerpartlemd  26749  rrvdmss  26832  refssfne  28566  islocfin  28568  neibastop3  28583  topmeet  28585  topjoin  28586  fnemeet2  28588  fnejoin1  28589  heiborlem3  28712  ssrecnpr  29594  lsatelbN  32651  lkrscss  32743  lshpset2N  32764  mapdrvallem2  35290  hdmaprnlem3eN  35506  hdmaplkr  35561