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

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

Proof of Theorem snsstp3
StepHypRef Expression
1 ssun2 3456 . 2  |-  { C }  C_  ( { A ,  B }  u.  { C } )
2 df-tp 3767 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
31, 2sseqtr4i 3326 1  |-  { C }  C_  { A ,  B ,  C }
Colors of variables: wff set class
Syntax hints:    u. cun 3263    C_ wss 3265   {csn 3759   {cpr 3760   {ctp 3761
This theorem is referenced by:  fr3nr  4702  rngmulr  13508  srngmulr  13516  lmodsca  13525  algmulr  13530  phlsca  13540  topgrptset  13548  otpsle  13555  odrngmulr  13566  odrngds  13569  prdsmulr  13611  prdsds  13615  imasds  13668  imasmulr  13673  fuccofval  14085  setccofval  14166  catccofval  14184  xpccofval  14208  psrmulr  16377  cnfldmul  16634  cnfldds  16638
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
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 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-un 3270  df-in 3272  df-ss 3279  df-tp 3767
  Copyright terms: Public domain W3C validator