Theorem snsstp3 4761

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

Syntax hints:   ∪ cun 3887   ⊆ wss 3889  {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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-tp 4572

This theorem is referenced by:  fr3nr  7726  rngmulr  17264  srngmulr  17275  lmodsca  17291  ipsmulr  17302  ipsip  17305  phlsca  17312  topgrptset  17327  otpsle  17342  odrngmulr  17369  odrngds  17372  prdsmulr  17422  prdsip  17424  prdsds  17427  imasds  17477  imasmulr  17482  imasip  17485  fuccofval  17929  setccofval  18049  catccofval  18071  estrccofval  18095  xpccofval  18148  mpocnfldmul  21359  cnfldds  21364  psrmulr  21921  trkgitv  28515  rlocmulval  33330  idlsrgmulr  33567  signswch  34705  algmulr  43604  clsk1indlem1  44472  rngccofvalALTV  48746  ringccofvalALTV  48780  catcofval  49703  mndtcco  50060