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

Theorem snsstp3 4317
Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
Assertion
Ref Expression
snsstp3 {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Proof of Theorem snsstp3
StepHypRef Expression
1 ssun2 3755 . 2 {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2 df-tp 4153 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
31, 2sseqtr4i 3617 1 {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3553  wss 3555  {csn 4148  {cpr 4150  {ctp 4152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-in 3562  df-ss 3569  df-tp 4153
This theorem is referenced by:  fr3nr  6926  rngmulr  15924  srngmulr  15932  lmodsca  15941  ipsmulr  15948  ipsip  15951  phlsca  15958  topgrptset  15966  otpsle  15975  otpsleOLD  15979  odrngmulr  15990  odrngds  15993  prdsmulr  16040  prdsip  16042  prdsds  16045  imasds  16094  imasmulr  16099  imasip  16102  fuccofval  16540  setccofval  16653  catccofval  16671  estrccofval  16690  xpccofval  16743  psrmulr  19303  cnfldmul  19671  cnfldds  19675  trkgitv  25246  signswch  30418  algmulr  37231  clsk1indlem1  37825  rngccofvalALTV  41275  ringccofvalALTV  41338
  Copyright terms: Public domain W3C validator