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

Theorem snsstp2 4163
Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
Assertion
Ref Expression
snsstp2  |-  { B }  C_  { A ,  B ,  C }

Proof of Theorem snsstp2
StepHypRef Expression
1 snsspr2 4161 . . 3  |-  { B }  C_  { A ,  B }
2 ssun1 3649 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3495 . 2  |-  { B }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 4015 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
53, 4sseqtr4i 3519 1  |-  { B }  C_  { A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    u. cun 3456    C_ wss 3458   {csn 4010   {cpr 4012   {ctp 4014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463  df-in 3465  df-ss 3472  df-pr 4013  df-tp 4015
This theorem is referenced by:  fr3nr  6596  rngplusg  14618  srngplusg  14626  lmodplusg  14635  ipsaddg  14642  ipsvsca  14645  phlplusg  14652  topgrpplusg  14660  otpstset  14667  odrngplusg  14678  odrngle  14681  prdsplusg  14727  prdsvsca  14729  prdsle  14731  imasplusg  14786  imasvsca  14789  imasle  14792  fuchom  15199  setchomfval  15275  catchomfval  15294  xpchomfval  15317  psrplusg  17902  psrvscafval  17911  cnfldadd  18293  cnfldle  18297  trkgdist  23707  algaddg  31097  estrchomfval  32471  rngchomfvalOLD  32511  ringchomfvalOLD  32567
  Copyright terms: Public domain W3C validator