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

Theorem snsstp3 4745
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 4148 . 2 {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2 df-tp 4564 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
31, 2sseqtrri 4003 1 {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3933  wss 3935  {csn 4559  {cpr 4561  {ctp 4563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3940  df-in 3942  df-ss 3951  df-tp 4564
This theorem is referenced by:  fr3nr  7482  rngmulr  16612  srngmulr  16620  lmodsca  16629  ipsmulr  16636  ipsip  16639  phlsca  16646  topgrptset  16654  otpsle  16661  odrngmulr  16672  odrngds  16675  prdsmulr  16722  prdsip  16724  prdsds  16727  imasds  16776  imasmulr  16781  imasip  16784  fuccofval  17219  setccofval  17332  catccofval  17350  estrccofval  17369  xpccofval  17422  psrmulr  20094  cnfldmul  20481  cnfldds  20485  trkgitv  26161  signswch  31731  algmulr  39660  clsk1indlem1  40275  rngccofvalALTV  44156  ringccofvalALTV  44219
  Copyright terms: Public domain W3C validator