Theorem snsstp3 4749

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

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4555  {cpr 4557  {ctp 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-tp 4560

This theorem is referenced by:  fr3nr  7715  rngmulr  17255  srngmulr  17266  lmodsca  17282  ipsmulr  17293  ipsip  17296  phlsca  17303  topgrptset  17318  otpsle  17333  odrngmulr  17360  odrngds  17363  prdsmulr  17413  prdsip  17415  prdsds  17418  imasds  17468  imasmulr  17473  imasip  17476  fuccofval  17920  setccofval  18040  catccofval  18062  estrccofval  18086  xpccofval  18139  mpocnfldmul  21354  cnfldds  21359  psrmulr  21917  trkgitv  28533  rlocmulval  33350  idlsrgmulr  33590  signswch  34745  algmulr  43621  clsk1indlem1  44489  rngccofvalALTV  48761  ringccofvalALTV  48795  catcofval  49718  mndtcco  50075