Theorem eqimss2 3361

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

Syntax hints:   -> wi 4   = wceq 1649   C_ wss 3280

This theorem is referenced by:  disjeq2  4146  disjeq1  4149  poeq2  4467  freq2  4513  seeq1  4514  seeq2  4515  suc11  4644  dmcoeq  5097  xp11  5263  funeq  5432  fconst3  5914  tposeq  6440  sorpssuni  6490  sorpssint  6491  oaass  6763  odi  6781  oen0  6788  inficl  7388  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnflem1d  7600  cantnflem1  7601  fodomfi2  7897  zorng  8340  rlimclim  12295  imasaddfnlem  13708  imasvscafn  13717  gasubg  15034  pgpssslw  15203  dprddisj2  15552  dprd2da  15555  ply1coe  16639  frgpcyg  16809  topgele  16954  topontopn  16962  toponmre  17112  conima  17441  ptbasfi  17566  txdis  17617  neifil  17865  elfm3  17935  rnelfmlem  17937  alexsubALTlem3  18033  alexsubALTlem4  18034  utopsnneiplem  18230  lmclimf  19209  uniiccdif  19423  dv11cn  19838  evlslem6  19887  plypf1  20084  subgores  21845  hstoh  23688  dmdi2  23760  rrvdmss  24660  refssfne  26264  islocfin  26266  neibastop3  26281  topmeet  26283  topjoin  26284  fnemeet2  26286  fnejoin1  26287  heiborlem3  26412  uvcresum  27110  ssrecnpr  27405  lsatelbN  29489  lkrscss  29581  lshpset2N  29602  mapdrvallem2  32128  hdmaprnlem3eN  32344  hdmaplkr  32399

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294