Theorem snsstp3 4772

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

Syntax hints:   ∪ cun 3897   ⊆ wss 3899  {csn 4578  {cpr 4580  {ctp 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-tp 4583

This theorem is referenced by:  fr3nr  7715  rngmulr  17219  srngmulr  17230  lmodsca  17246  ipsmulr  17257  ipsip  17260  phlsca  17267  topgrptset  17282  otpsle  17297  odrngmulr  17324  odrngds  17327  prdsmulr  17377  prdsip  17379  prdsds  17382  imasds  17432  imasmulr  17437  imasip  17440  fuccofval  17884  setccofval  18004  catccofval  18026  estrccofval  18050  xpccofval  18103  mpocnfldmul  21314  cnfldds  21319  cnfldmulOLD  21328  cnflddsOLD  21332  psrmulr  21896  trkgitv  28468  rlocmulval  33300  idlsrgmulr  33537  signswch  34667  algmulr  43360  clsk1indlem1  44228  rngccofvalALTV  48458  ringccofvalALTV  48492  catcofval  49415  mndtcco  49772