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

Syntax hints:   ∪ cun 3902   ⊆ wss 3904  {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 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-tp 4587

This theorem is referenced by:  fr3nr  7755  rngmulr  17330  srngmulr  17341  lmodsca  17357  ipsmulr  17368  ipsip  17371  phlsca  17378  topgrptset  17393  otpsle  17408  odrngmulr  17435  odrngds  17438  prdsmulr  17488  prdsip  17490  prdsds  17493  imasds  17543  imasmulr  17548  imasip  17551  fuccofval  17995  setccofval  18115  catccofval  18137  estrccofval  18161  xpccofval  18214  mpocnfldmul  21431  cnfldds  21436  psrmulr  21994  trkgitv  28616  rlocmulval  33451  idlsrgmulr  33703  signswch  34855  algmulr  43753  clsk1indlem1  44621  rngccofvalALTV  48892  ringccofvalALTV  48926  catcofval  49849  mndtcco  50206