Theorem snsstp3 4502

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 3938	. 2 ⊢ {𝐶} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
2		df-tp 4338	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sseqtr4i 3797	1 ⊢ {𝐶} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3729   ⊆ wss 3731  {csn 4333  {cpr 4335  {ctp 4337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2742

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-v 3351  df-un 3736  df-in 3738  df-ss 3745  df-tp 4338

This theorem is referenced by:  fr3nr  7176  rngmulr  16276  srngmulr  16284  lmodsca  16293  ipsmulr  16300  ipsip  16303  phlsca  16310  topgrptset  16318  otpsle  16325  odrngmulr  16336  odrngds  16339  prdsmulr  16386  prdsip  16388  prdsds  16391  imasds  16440  imasmulr  16445  imasip  16448  fuccofval  16885  setccofval  16998  catccofval  17016  estrccofval  17035  xpccofval  17089  psrmulr  19657  cnfldmul  20024  cnfldds  20028  trkgitv  25636  signswch  31020  algmulr  38359  clsk1indlem1  38949  rngccofvalALTV  42588  ringccofvalALTV  42651