Theorem snsstp3 4770

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 4125	. 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2		df-tp 4583	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sseqtrri 3973	1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3900   ⊆ wss 3902  {csn 4578  {cpr 4580  {ctp 4582

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-un 3907  df-in 3909  df-ss 3919  df-tp 4583

This theorem is referenced by:  fr3nr  7689  rngmulr  17109  srngmulr  17120  lmodsca  17136  ipsmulr  17147  ipsip  17150  phlsca  17157  topgrptset  17172  otpsle  17187  odrngmulr  17214  odrngds  17217  prdsmulr  17268  prdsip  17270  prdsds  17273  imasds  17322  imasmulr  17327  imasip  17330  fuccofval  17774  setccofval  17895  catccofval  17917  estrccofval  17943  xpccofval  17997  cnfldmul  20709  cnfldds  20713  psrmulr  21259  trkgitv  27097  idlsrgmulr  31947  signswch  32838  algmulr  41317  clsk1indlem1  42026  rngccofvalALTV  45961  ringccofvalALTV  46024  mndtcco  46788