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

Theorem snsstp2 3974
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 3972 . . 3  |-  { B }  C_  { A ,  B }
2 ssun1 3496 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3343 . 2  |-  { B }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 3846 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
53, 4sseqtr4i 3367 1  |-  { B }  C_  { A ,  B ,  C }
Colors of variables: wff set class
Syntax hints:    u. cun 3304    C_ wss 3306   {csn 3838   {cpr 3839   {ctp 3840
This theorem is referenced by:  fr3nr  4789  rngplusg  13609  srngplusg  13617  lmodplusg  13626  algaddg  13631  phlplusg  13641  topgrpplusg  13649  otpstset  13656  odrngplusg  13667  odrngle  13670  prdsplusg  13712  prdsle  13715  imasplusg  13774  imasle  13779  fuchom  14189  setchomfval  14265  catchomfval  14284  xpchomfval  14307  psrplusg  16476  psrvscafval  16485  cnfldadd  16739  cnfldle  16743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
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 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311  df-in 3313  df-ss 3320  df-pr 3845  df-tp 3846
  Copyright terms: Public domain W3C validator