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

Theorem snsstp3 4180
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 3668 . 2  |-  { C }  C_  ( { A ,  B }  u.  { C } )
2 df-tp 4032 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
31, 2sseqtr4i 3537 1  |-  { C }  C_  { A ,  B ,  C }
Colors of variables: wff setvar class
Syntax hints:    u. cun 3474    C_ wss 3476   {csn 4027   {cpr 4029   {ctp 4031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-tp 4032
This theorem is referenced by:  fr3nr  6593  rngmulr  14601  srngmulr  14609  lmodsca  14618  ipsmulr  14625  ipsip  14628  phlsca  14635  topgrptset  14643  otpsle  14650  odrngmulr  14661  odrngds  14664  prdsmulr  14710  prdsip  14712  prdsds  14715  imasds  14764  imasmulr  14769  imasip  14772  fuccofval  15182  setccofval  15263  catccofval  15281  xpccofval  15305  psrmulr  17808  cnfldmul  18197  cnfldds  18201  trkgitv  23571  signswch  28158  algmulr  30734
  Copyright terms: Public domain W3C validator