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

Theorem snsstp3 4502
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 3938 . 2 {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2 df-tp 4338 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
31, 2sseqtr4i 3797 1 {𝐶} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3729  wss 3731  {csn 4333  {cpr 4335  {ctp 4337
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-v 3351  df-un 3736  df-in 3738  df-ss 3745  df-tp 4338
This theorem is referenced by:  fr3nr  7176  rngmulr  16276  srngmulr  16284  lmodsca  16293  ipsmulr  16300  ipsip  16303  phlsca  16310  topgrptset  16318  otpsle  16325  odrngmulr  16336  odrngds  16339  prdsmulr  16386  prdsip  16388  prdsds  16391  imasds  16440  imasmulr  16445  imasip  16448  fuccofval  16885  setccofval  16998  catccofval  17016  estrccofval  17035  xpccofval  17089  psrmulr  19657  cnfldmul  20024  cnfldds  20028  trkgitv  25636  signswch  31020  algmulr  38359  clsk1indlem1  38949  rngccofvalALTV  42588  ringccofvalALTV  42651
  Copyright terms: Public domain W3C validator