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  17900  setccofval  18020  catccofval  18042  estrccofval  18066  xpccofval  18119  mpocnfldmul  21247  cnfldds  21252  cnfldmulOLD  21261  cnflddsOLD  21265  psrmulr  21827  trkgitv  28350  rlocmulval  33193  idlsrgmulr  33451  signswch  34525  algmulr  43138  clsk1indlem1  44007  rngccofvalALTV  48231  ringccofvalALTV  48265  catcofval  49190  mndtcco  49547