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

Theorem snsstp3 3953
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 3513 . 2  |-  { C }  C_  ( { A ,  B }  u.  { C } )
2 df-tp 3824 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
31, 2sseqtr4i 3383 1  |-  { C }  C_  { A ,  B ,  C }
Colors of variables: wff set class
Syntax hints:    u. cun 3320    C_ wss 3322   {csn 3816   {cpr 3817   {ctp 3818
This theorem is referenced by:  fr3nr  4763  rngmulr  13584  srngmulr  13592  lmodsca  13601  algmulr  13606  phlsca  13616  topgrptset  13624  otpsle  13631  odrngmulr  13642  odrngds  13645  prdsmulr  13687  prdsds  13691  imasds  13744  imasmulr  13749  fuccofval  14161  setccofval  14242  catccofval  14260  xpccofval  14284  psrmulr  16453  cnfldmul  16714  cnfldds  16718
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 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-in 3329  df-ss 3336  df-tp 3824
  Copyright terms: Public domain W3C validator