Theorem snsstp3 4778

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

Syntax hints:   ∪ cun 3909   ⊆ wss 3911  {csn 4585  {cpr 4587  {ctp 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928  df-tp 4590

This theorem is referenced by:  fr3nr  7728  rngmulr  17240  srngmulr  17251  lmodsca  17267  ipsmulr  17278  ipsip  17281  phlsca  17288  topgrptset  17303  otpsle  17318  odrngmulr  17345  odrngds  17348  prdsmulr  17398  prdsip  17400  prdsds  17403  imasds  17452  imasmulr  17457  imasip  17460  fuccofval  17904  setccofval  18024  catccofval  18046  estrccofval  18070  xpccofval  18123  mpocnfldmul  21303  cnfldds  21308  cnfldmulOLD  21317  cnflddsOLD  21321  psrmulr  21884  trkgitv  28427  rlocmulval  33236  idlsrgmulr  33471  signswch  34545  algmulr  43158  clsk1indlem1  44027  rngccofvalALTV  48251  ringccofvalALTV  48285  catcofval  49210  mndtcco  49567