Theorem snsstp3 4776

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

This proof depends on syntax axioms:   ⊆ wss 3899   ∪ cun 4151  {csn 4587  {cpr 4589  {ctp 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-un 4153  df-tp 4592

This theorem is used by:  fr3nr  7793  rngmulr  17484  srngmulr  17495  lmodsca  17511  ipsmulr  17522  ipsip  17525  phlsca  17532  topgrptset  17547  otpsle  17562  odrngmulr  17589  odrngds  17592  prdsmulr  17642  prdsip  17644  prdsds  17647  imasds  17697  imasmulr  17702  imasip  17705  fuccofval  18149  setccofval  18269  catccofval  18291  estrccofval  18315  xpccofval  18368  mpocnfldmul  21697  cnfldds  21702  psrmulr  22262  trkgitv  28921  rlocmulval  33884  idlsrgmulr  34092  signswch  35243  algmulr  44318  clsk1indlem1  45185  rngccofvalALTV  49506  ringccofvalALTV  49540  catcofval  50489  mndtcco  50862