Theorem snsstp3 4820

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

Syntax hints:   ∪ cun 3945   ⊆ wss 3947  {csn 4627  {cpr 4629  {ctp 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952  df-in 3954  df-ss 3964  df-tp 4632

This theorem is referenced by:  fr3nr  7761  rngmulr  17250  srngmulr  17261  lmodsca  17277  ipsmulr  17288  ipsip  17291  phlsca  17298  topgrptset  17313  otpsle  17328  odrngmulr  17355  odrngds  17358  prdsmulr  17409  prdsip  17411  prdsds  17414  imasds  17463  imasmulr  17468  imasip  17471  fuccofval  17915  setccofval  18036  catccofval  18058  estrccofval  18084  xpccofval  18138  cnfldmul  21150  cnfldds  21154  psrmulr  21722  trkgitv  27965  idlsrgmulr  32895  signswch  33870  mpocnfldmul  35477  gg-cnfldds  35481  algmulr  42224  clsk1indlem1  43098  rngccofvalALTV  46973  ringccofvalALTV  47036  mndtcco  47798