Theorem snsstp3 4751

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

Step	Hyp	Ref	Expression
1		ssun2 4107	. 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2		df-tp 4566	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sseqtrri 3958	1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3885   ⊆ wss 3887  {csn 4561  {cpr 4563  {ctp 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-tp 4566

This theorem is referenced by:  fr3nr  7622  rngmulr  17011  srngmulr  17022  lmodsca  17038  ipsmulr  17049  ipsip  17052  phlsca  17059  topgrptset  17074  otpsle  17089  odrngmulr  17116  odrngds  17119  prdsmulr  17170  prdsip  17172  prdsds  17175  imasds  17224  imasmulr  17229  imasip  17232  fuccofval  17676  setccofval  17797  catccofval  17819  estrccofval  17845  xpccofval  17899  cnfldmul  20603  cnfldds  20607  psrmulr  21153  trkgitv  26808  idlsrgmulr  31652  signswch  32540  algmulr  41005  clsk1indlem1  41655  rngccofvalALTV  45545  ringccofvalALTV  45608  mndtcco  46372