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

Theorem snsstp2 3918
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 3916 . . 3  |-  { B }  C_  { A ,  B }
2 ssun1 3478 . . 3  |-  { A ,  B }  C_  ( { A ,  B }  u.  { C } )
31, 2sstri 3325 . 2  |-  { B }  C_  ( { A ,  B }  u.  { C } )
4 df-tp 3790 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
53, 4sseqtr4i 3349 1  |-  { B }  C_  { A ,  B ,  C }
Colors of variables: wff set class
Syntax hints:    u. cun 3286    C_ wss 3288   {csn 3782   {cpr 3783   {ctp 3784
This theorem is referenced by:  fr3nr  4727  rngplusg  13541  srngplusg  13549  lmodplusg  13558  algaddg  13563  phlplusg  13573  topgrpplusg  13581  otpstset  13588  odrngplusg  13599  odrngle  13602  prdsplusg  13644  prdsle  13647  imasplusg  13706  imasle  13711  fuchom  14121  setchomfval  14197  catchomfval  14216  xpchomfval  14239  psrplusg  16408  psrvscafval  16417  cnfldadd  16671  cnfldle  16675
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-un 3293  df-in 3295  df-ss 3302  df-pr 3789  df-tp 3790
  Copyright terms: Public domain W3C validator