Theorem snsstp3 4789

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

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {csn 4594  {cpr 4596  {ctp 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-v 3464  df-un 3918  df-ss 3930  df-tp 4599

This theorem is referenced by:  fr3nr  7774  rngmulr  17357  srngmulr  17368  lmodsca  17384  ipsmulr  17395  ipsip  17398  phlsca  17405  topgrptset  17420  otpsle  17435  odrngmulr  17462  odrngds  17465  prdsmulr  17515  prdsip  17517  prdsds  17520  imasds  17570  imasmulr  17575  imasip  17578  fuccofval  18022  setccofval  18142  catccofval  18164  estrccofval  18188  xpccofval  18241  mpocnfldmul  21512  cnfldds  21517  psrmulr  22075  trkgitv  28696  rlocmulval  33560  idlsrgmulr  33767  signswch  34918  algmulr  43855  clsk1indlem1  44723  rngccofvalALTV  48984  ringccofvalALTV  49018  catcofval  49955  mndtcco  50312