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

Theorem snsstp2 3865
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 3863 . . 3  |-  { B }  C_  { A ,  B }
2 ssun1 3426 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3274 . 2  |-  { B }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 3737 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
53, 4sseqtr4i 3297 1  |-  { B }  C_  { A ,  B ,  C }
Colors of variables: wff set class
Syntax hints:    u. cun 3236    C_ wss 3238   {csn 3729   {cpr 3730   {ctp 3731
This theorem is referenced by:  fr3nr  4674  rngplusg  13465  srngplusg  13473  lmodplusg  13482  algaddg  13487  phlplusg  13497  topgrpplusg  13505  otpstset  13512  odrngplusg  13523  odrngle  13526  prdsplusg  13568  prdsle  13571  imasplusg  13630  imasle  13635  fuchom  14045  setchomfval  14121  catchomfval  14140  xpchomfval  14163  psrplusg  16336  psrvscafval  16345  cnfldadd  16598  cnfldle  16602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-un 3243  df-in 3245  df-ss 3252  df-pr 3736  df-tp 3737
  Copyright terms: Public domain W3C validator