Theorem snsstp3 4485

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

Syntax hints:   ∪ cun 3721   ⊆ wss 3723  {csn 4317  {cpr 4319  {ctp 4321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-tp 4322

This theorem is referenced by:  fr3nr  7130  rngmulr  16211  srngmulr  16219  lmodsca  16228  ipsmulr  16235  ipsip  16238  phlsca  16245  topgrptset  16253  otpsle  16262  otpsleOLD  16266  odrngmulr  16277  odrngds  16280  prdsmulr  16327  prdsip  16329  prdsds  16332  imasds  16381  imasmulr  16386  imasip  16389  fuccofval  16826  setccofval  16939  catccofval  16957  estrccofval  16976  xpccofval  17030  psrmulr  19599  cnfldmul  19967  cnfldds  19971  trkgitv  25567  signswch  30978  algmulr  38274  clsk1indlem1  38867  rngccofvalALTV  42510  ringccofvalALTV  42573