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

Theorem snsstp3 4711
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 4100 . 2 {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2 df-tp 4530 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
31, 2sseqtrri 3952 1 {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3879  wss 3881  {csn 4525  {cpr 4527  {ctp 4529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-tp 4530
This theorem is referenced by:  fr3nr  7474  rngmulr  16614  srngmulr  16622  lmodsca  16631  ipsmulr  16638  ipsip  16641  phlsca  16648  topgrptset  16656  otpsle  16663  odrngmulr  16674  odrngds  16677  prdsmulr  16724  prdsip  16726  prdsds  16729  imasds  16778  imasmulr  16783  imasip  16786  fuccofval  17221  setccofval  17334  catccofval  17352  estrccofval  17371  xpccofval  17424  cnfldmul  20097  cnfldds  20101  psrmulr  20622  trkgitv  26241  idlsrgmulr  31060  signswch  31941  algmulr  40122  clsk1indlem1  40746  rngccofvalALTV  44609  ringccofvalALTV  44672
  Copyright terms: Public domain W3C validator