Theorem snsstp3 4751

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

Syntax hints:   ∪ cun 3934   ⊆ wss 3936  {csn 4567  {cpr 4569  {ctp 4571

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-tp 4572

This theorem is referenced by:  fr3nr  7494  rngmulr  16622  srngmulr  16630  lmodsca  16639  ipsmulr  16646  ipsip  16649  phlsca  16656  topgrptset  16664  otpsle  16671  odrngmulr  16682  odrngds  16685  prdsmulr  16732  prdsip  16734  prdsds  16737  imasds  16786  imasmulr  16791  imasip  16794  fuccofval  17229  setccofval  17342  catccofval  17360  estrccofval  17379  xpccofval  17432  psrmulr  20164  cnfldmul  20551  cnfldds  20555  trkgitv  26233  signswch  31831  algmulr  39800  clsk1indlem1  40415  rngccofvalALTV  44278  ringccofvalALTV  44341