Theorem snsstp3 4717

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

Syntax hints:   ∪ cun 3851   ⊆ wss 3853  {csn 4527  {cpr 4529  {ctp 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870  df-tp 4532

This theorem is referenced by:  fr3nr  7535  rngmulr  16806  srngmulr  16814  lmodsca  16823  ipsmulr  16830  ipsip  16833  phlsca  16840  topgrptset  16848  otpsle  16855  odrngmulr  16867  odrngds  16870  prdsmulr  16918  prdsip  16920  prdsds  16923  imasds  16972  imasmulr  16977  imasip  16980  fuccofval  17421  setccofval  17542  catccofval  17564  estrccofval  17590  xpccofval  17643  cnfldmul  20323  cnfldds  20327  psrmulr  20863  trkgitv  26492  idlsrgmulr  31320  signswch  32206  algmulr  40649  clsk1indlem1  41273  rngccofvalALTV  45161  ringccofvalALTV  45224  mndtcco  45986