Theorem snsstp3 4748

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

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4558  {cpr 4560  {ctp 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-tp 4563

This theorem is referenced by:  fr3nr  7600  rngmulr  16937  srngmulr  16948  lmodsca  16964  ipsmulr  16974  ipsip  16977  phlsca  16984  topgrptset  16998  otpsle  17012  odrngmulr  17035  odrngds  17038  prdsmulr  17087  prdsip  17089  prdsds  17092  imasds  17141  imasmulr  17146  imasip  17149  fuccofval  17592  setccofval  17713  catccofval  17735  estrccofval  17761  xpccofval  17815  cnfldmul  20516  cnfldds  20520  psrmulr  21063  trkgitv  26712  idlsrgmulr  31554  signswch  32440  algmulr  40921  clsk1indlem1  41544  rngccofvalALTV  45433  ringccofvalALTV  45496  mndtcco  46258