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

Theorem snsstp3 4823
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 4171 . 2 {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2 df-tp 4635 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
31, 2sseqtrri 4014 1 {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3942  wss 3944  {csn 4630  {cpr 4632  {ctp 4634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-ss 3961  df-tp 4635
This theorem is referenced by:  fr3nr  7775  rngmulr  17285  srngmulr  17296  lmodsca  17312  ipsmulr  17323  ipsip  17326  phlsca  17333  topgrptset  17348  otpsle  17363  odrngmulr  17390  odrngds  17393  prdsmulr  17444  prdsip  17446  prdsds  17449  imasds  17498  imasmulr  17503  imasip  17506  fuccofval  17953  setccofval  18074  catccofval  18096  estrccofval  18122  xpccofval  18176  mpocnfldmul  21303  cnfldds  21308  cnfldmulOLD  21317  cnflddsOLD  21321  psrmulr  21904  trkgitv  28323  rlocmulval  33059  idlsrgmulr  33319  signswch  34324  algmulr  42746  clsk1indlem1  43617  rngccofvalALTV  47518  ringccofvalALTV  47552  mndtcco  48283
  Copyright terms: Public domain W3C validator