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

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152  {csn 4588  {cpr 4590  {ctp 4592

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-tp 4593

This theorem is used by:  fr3nr  7818  rngmulr  17518  srngmulr  17529  lmodsca  17545  ipsmulr  17556  ipsip  17559  phlsca  17566  topgrptset  17581  otpsle  17596  odrngmulr  17623  odrngds  17626  prdsmulr  17680  prdsip  17682  prdsds  17685  imasds  17735  imasmulr  17740  imasip  17743  fuccofval  18187  setccofval  18307  catccofval  18329  estrccofval  18353  xpccofval  18406  mpocnfldmul  21736  cnfldds  21741  psrmulr  22305  trkgitv  28966  rlocmulval  33930  idlsrgmulr  34143  signswch  35301  algmulr  44439  clsk1indlem1  45306  rngccofvalALTV  49640  ringccofvalALTV  49674  catcofval  50681  mndtcco  51054