Theorem snsstp3 4782

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

Syntax hints:   ∪ cun 3912   ⊆ wss 3914  {csn 4589  {cpr 4591  {ctp 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-tp 4594

This theorem is referenced by:  fr3nr  7748  rngmulr  17264  srngmulr  17275  lmodsca  17291  ipsmulr  17302  ipsip  17305  phlsca  17312  topgrptset  17327  otpsle  17342  odrngmulr  17369  odrngds  17372  prdsmulr  17422  prdsip  17424  prdsds  17427  imasds  17476  imasmulr  17481  imasip  17484  fuccofval  17924  setccofval  18044  catccofval  18066  estrccofval  18090  xpccofval  18143  mpocnfldmul  21271  cnfldds  21276  cnfldmulOLD  21285  cnflddsOLD  21289  psrmulr  21851  trkgitv  28374  rlocmulval  33220  idlsrgmulr  33478  signswch  34552  algmulr  43165  clsk1indlem1  44034  rngccofvalALTV  48258  ringccofvalALTV  48292  catcofval  49217  mndtcco  49574