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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-tp 4589

This theorem is used by:  fr3nr  7772  rngmulr  17389  srngmulr  17400  lmodsca  17416  ipsmulr  17427  ipsip  17430  phlsca  17437  topgrptset  17452  otpsle  17467  odrngmulr  17494  odrngds  17497  prdsmulr  17547  prdsip  17549  prdsds  17552  imasds  17602  imasmulr  17607  imasip  17610  fuccofval  18054  setccofval  18174  catccofval  18196  estrccofval  18220  xpccofval  18273  mpocnfldmul  21595  cnfldds  21600  psrmulr  22160  trkgitv  28791  rlocmulval  33713  idlsrgmulr  33920  signswch  35072  algmulr  44020  clsk1indlem1  44888  rngccofvalALTV  49188  ringccofvalALTV  49222  catcofval  50157  mndtcco  50514