MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snssi Structured version   Unicode version

Theorem snssi 3944
Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
snssi  |-  ( A  e.  B  ->  { A }  C_  B )

Proof of Theorem snssi
StepHypRef Expression
1 snssg 3934 . 2  |-  ( A  e.  B  ->  ( A  e.  B  <->  { A }  C_  B ) )
21ibi 234 1  |-  ( A  e.  B  ->  { A }  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    C_ wss 3322   {csn 3816
This theorem is referenced by:  difsnid  3946  pwpw0  3948  sssn  3959  ssunsn2  3960  tpssi  3967  pwsnALT  4012  snelpwi  4411  intid  4423  suceloni  4795  xpsspw  4988  xpsspwOLD  4989  djussxp  5020  xpimasn  5318  fconst6g  5634  dffv2  5798  fvimacnvi  5846  fvimacnvALT  5851  fsn2  5910  fsnunf  5933  curry1  6440  curry2  6443  mapsn  7057  fodomr  7260  sucdom2  7305  en1eqsn  7340  enp1ilem  7344  findcard2  7350  findcard2s  7351  marypha1lem  7440  marypha2lem1  7442  epfrs  7669  dfac5lem4  8009  kmlem11  8042  ackbij1lem2  8103  fin23lem26  8207  isfin1-3  8268  hsmexlem4  8311  axdc3lem4  8335  axresscn  9025  nn0ssre  10227  xrsupss  10889  supxrmnf  10898  1fv  11122  1exp  11411  hashxrcl  11642  hashdifsn  11681  brfi1indlem  11716  s1cl  11757  fsum00  12579  incexc  12619  xpnnenOLD  12811  2ebits  12961  bitsinvp1  12963  4sqlem19  13333  ramxrcl  13387  strlemor1  13558  mrcsncl  13839  acsfn1  13888  homaf  14187  dmcoass  14223  lubel  14551  gsumws1  14787  cycsubg2  14979  cntzsnval  15125  0frgp  15413  dpjidcl  15618  ablfac1eu  15633  lspsncl  16055  lspsnss  16068  lspsnid  16071  lpival  16318  lpiss  16323  lidldvgen  16328  znlidl  16816  frgpcyg  16856  isneip  17171  neips  17179  opnneip  17185  maxlp  17213  restsn2  17237  leordtval2  17278  ist1-3  17415  ordtt1  17445  2ndcdisj2  17522  uffix  17955  neiflim  18008  ptcmplem5  18089  cnextfres  18101  haustsms2  18168  ust0  18251  ustuqtop5  18277  dscopn  18623  icccmplem1  18855  bndth  18985  ovolsn  19393  icombl1  19459  plyun0  20118  coeeulem  20145  coeeu  20146  vieta1lem2  20230  aalioulem2  20252  taylfval  20277  perfectlem2  21016  konigsberg  21711  hsn0elch  22752  chsupsn  22917  chsup0  23052  h1deoi  23053  h1dei  23054  h1did  23055  h1de2ctlem  23059  h1de2ci  23060  spansni  23061  spansnch  23064  elspansncl  23069  spansnpji  23082  spanunsni  23083  spanpr  23084  h1datomi  23085  spansnji  23150  h1da  23854  atom1d  23858  superpos  23859  esumnul  24445  esumcst  24457  hashf2  24476  measvuni  24570  cntnevol  24584  ballotlemfp1  24751  dfon2lem3  25414  altxpsspw  25824  axlowdimlem7  25889  axlowdimlem10  25892  mblfinlem2  26246  dvreasin  26292  fdc  26451  prnc  26679  isfldidl  26680  ispridlc  26682  ralxpmap  26744  mapfzcons  26774  mzpcompact2lem  26810  diophrw  26819  frlmlbs  27228  stoweidlem44  27771  dmressnsn  27963  fnbrafvb  27996  afvres  28014  snelpwrVD  29005  islshpsm  29840  snatpsubN  30609  polatN  30790  atpsubclN  30804  pclfinclN  30809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336  df-sn 3822
  Copyright terms: Public domain W3C validator