Theorem snsstp3 4289

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 3739	. 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2		df-tp 4130	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sseqtr4i 3601	1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3538   ⊆ wss 3540  {csn 4125  {cpr 4127  {ctp 4129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-tp 4130

This theorem is referenced by:  fr3nr  6871  rngmulr  15826  srngmulr  15834  lmodsca  15843  ipsmulr  15850  ipsip  15853  phlsca  15860  topgrptset  15868  otpsle  15877  otpsleOLD  15881  odrngmulr  15892  odrngds  15895  prdsmulr  15942  prdsip  15944  prdsds  15947  imasds  15996  imasmulr  16001  imasip  16004  fuccofval  16442  setccofval  16555  catccofval  16573  estrccofval  16592  xpccofval  16645  psrmulr  19205  cnfldmul  19573  cnfldds  19577  trkgitv  25146  signswch  29964  algmulr  36769  clsk1indlem1  37363  rngccofvalALTV  41779  ringccofvalALTV  41842