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

Theorem snsstp3 4168
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 3653 . 2  |-  { C }  C_  ( { A ,  B }  u.  { C } )
2 df-tp 4019 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
31, 2sseqtr4i 3522 1  |-  { C }  C_  { A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    u. cun 3459    C_ wss 3461   {csn 4014   {cpr 4016   {ctp 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475  df-tp 4019
This theorem is referenced by:  fr3nr  6600  rngmulr  14624  srngmulr  14632  lmodsca  14641  ipsmulr  14648  ipsip  14651  phlsca  14658  topgrptset  14666  otpsle  14673  odrngmulr  14684  odrngds  14687  prdsmulr  14733  prdsip  14735  prdsds  14738  imasds  14787  imasmulr  14792  imasip  14795  fuccofval  15202  setccofval  15283  catccofval  15301  xpccofval  15325  psrmulr  17911  cnfldmul  18300  cnfldds  18304  trkgitv  23715  signswch  28391  algmulr  31105  estrccofval  32484  rngccofvalOLD  32535  ringccofvalOLD  32595
  Copyright terms: Public domain W3C validator