Theorem snsstp3 4823

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

Syntax hints:   ∪ cun 3961   ⊆ wss 3963  {csn 4631  {cpr 4633  {ctp 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-tp 4636

This theorem is referenced by:  fr3nr  7791  rngmulr  17347  srngmulr  17358  lmodsca  17374  ipsmulr  17385  ipsip  17388  phlsca  17395  topgrptset  17410  otpsle  17425  odrngmulr  17452  odrngds  17455  prdsmulr  17506  prdsip  17508  prdsds  17511  imasds  17560  imasmulr  17565  imasip  17568  fuccofval  18015  setccofval  18136  catccofval  18158  estrccofval  18184  xpccofval  18238  mpocnfldmul  21389  cnfldds  21394  cnfldmulOLD  21403  cnflddsOLD  21407  psrmulr  21980  trkgitv  28470  rlocmulval  33256  idlsrgmulr  33515  signswch  34555  algmulr  43165  clsk1indlem1  44035  rngccofvalALTV  48114  ringccofvalALTV  48148  mndtcco  48894