Theorem eqimss2 3497

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

Syntax hints:   -> wi 4   = wceq 1455   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430

This theorem is referenced by:  disjeq2  4391  disjeq1  4394  poeq2  4778  freq2  4824  seeq1  4825  seeq2  4826  dmcoeq  5116  xp11  5291  suc11  5545  funeq  5620  fconst3  6153  sorpssuni  6607  sorpssint  6608  tposeq  7001  oaass  7288  odi  7306  oen0  7313  inficl  7965  cantnfp1lem1  8209  cantnflem1  8220  fodomfi2  8517  zorng  8960  rlimclim  13659  imasaddfnlem  15483  imasvscafn  15492  gasubg  17005  pgpssslw  17315  dprddisj2  17721  dprd2da  17724  evlslem6  18785  topgele  19998  topontopn  20006  toponmre  20158  conima  20489  islocfin  20581  ptbasfi  20645  txdis  20696  neifil  20944  elfm3  21014  rnelfmlem  21016  alexsubALTlem3  21113  alexsubALTlem4  21114  utopsnneiplem  21311  lmclimf  22322  uniiccdif  22584  dv11cn  23002  plypf1  23215  subgores  26081  hstoh  27934  dmdi2  28006  disjeq1f  28233  eulerpartlemd  29248  rrvdmss  29331  refssfne  31063  neibastop3  31067  topmeet  31069  topjoin  31070  fnemeet2  31072  fnejoin1  31073  heiborlem3  32190  lsatelbN  32617  lkrscss  32709  lshpset2N  32730  mapdrvallem2  35258  hdmaprnlem3eN  35474  hdmaplkr  35529  ssrecnpr  36700  founiiun  37484  founiiun0  37503  caragendifcl  38373  1wlkvtxiedg  39687  wlk1wlk  39699  2pthon3v-av  39892