Theorem snsstp3 4779

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

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899  {csn 4584  {cpr 4586  {ctp 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-tp 4589

This theorem is used by:  fr3nr  7786  rngmulr  17472  srngmulr  17483  lmodsca  17499  ipsmulr  17510  ipsip  17513  phlsca  17520  topgrptset  17535  otpsle  17550  odrngmulr  17577  odrngds  17580  prdsmulr  17630  prdsip  17632  prdsds  17635  imasds  17685  imasmulr  17690  imasip  17693  fuccofval  18137  setccofval  18257  catccofval  18279  estrccofval  18303  xpccofval  18356  mpocnfldmul  21685  cnfldds  21690  psrmulr  22250  trkgitv  28909  rlocmulval  33831  idlsrgmulr  34039  signswch  35190  algmulr  44177  clsk1indlem1  45044  rngccofvalALTV  49366  ringccofvalALTV  49400  catcofval  50335  mndtcco  50692