Theorem eqimss2 3557

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

Syntax hints:   -> wi 4   = wceq 1379   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  disjeq2  4421  disjeq1  4424  poeq2  4804  freq2  4850  seeq1  4851  seeq2  4852  suc11  4981  dmcoeq  5265  xp11  5442  funeq  5607  fconst3  6125  sorpssuni  6574  sorpssint  6575  tposeq  6958  oaass  7211  odi  7229  oen0  7236  inficl  7886  cantnfp1lem1  8098  cantnflem1  8109  cantnfp1lem1OLD  8124  cantnfp1lem3OLD  8126  cantnflem1dOLD  8131  cantnflem1OLD  8132  fodomfi2  8442  zorng  8885  rlimclim  13335  imasaddfnlem  14786  imasvscafn  14795  gasubg  16154  pgpssslw  16449  dprddisj2  16901  dprddisj2OLD  16902  dprd2da  16905  evlslem6  17992  evlslem6OLD  17993  topgele  19242  topontopn  19250  toponmre  19400  conima  19732  refssfne  19844  islocfin  19846  ptbasfi  19909  txdis  19960  neifil  20208  elfm3  20278  rnelfmlem  20280  alexsubALTlem3  20376  alexsubALTlem4  20377  utopsnneiplem  20577  lmclimf  21569  uniiccdif  21814  dv11cn  22229  plypf1  22436  subgores  25079  hstoh  26924  dmdi2  26996  eulerpartlemd  28056  rrvdmss  28139  neibastop3  30010  topmeet  30012  topjoin  30013  fnemeet2  30015  fnejoin1  30016  heiborlem3  30139  ssrecnpr  31018  lsatelbN  34020  lkrscss  34112  lshpset2N  34133  mapdrvallem2  36659  hdmaprnlem3eN  36875  hdmaplkr  36930