Theorem snsstp3 4776

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

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4582  {cpr 4584  {ctp 4586

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-tp 4587

This theorem is referenced by:  fr3nr  7727  rngmulr  17233  srngmulr  17244  lmodsca  17260  ipsmulr  17271  ipsip  17274  phlsca  17281  topgrptset  17296  otpsle  17311  odrngmulr  17338  odrngds  17341  prdsmulr  17391  prdsip  17393  prdsds  17396  imasds  17446  imasmulr  17451  imasip  17454  fuccofval  17898  setccofval  18018  catccofval  18040  estrccofval  18064  xpccofval  18117  mpocnfldmul  21328  cnfldds  21333  cnfldmulOLD  21342  cnflddsOLD  21346  psrmulr  21910  trkgitv  28531  rlocmulval  33363  idlsrgmulr  33600  signswch  34739  algmulr  43533  clsk1indlem1  44401  rngccofvalALTV  48630  ringccofvalALTV  48664  catcofval  49587  mndtcco  49944