Theorem snsstp3 4843

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

Syntax hints:   ∪ cun 3974   ⊆ wss 3976  {csn 4648  {cpr 4650  {ctp 4652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-tp 4653

This theorem is referenced by:  fr3nr  7807  rngmulr  17360  srngmulr  17371  lmodsca  17387  ipsmulr  17398  ipsip  17401  phlsca  17408  topgrptset  17423  otpsle  17438  odrngmulr  17465  odrngds  17468  prdsmulr  17519  prdsip  17521  prdsds  17524  imasds  17573  imasmulr  17578  imasip  17581  fuccofval  18028  setccofval  18149  catccofval  18171  estrccofval  18197  xpccofval  18251  mpocnfldmul  21394  cnfldds  21399  cnfldmulOLD  21408  cnflddsOLD  21412  psrmulr  21985  trkgitv  28473  rlocmulval  33241  idlsrgmulr  33500  signswch  34538  algmulr  43137  clsk1indlem1  44007  rngccofvalALTV  47993  ringccofvalALTV  48027  mndtcco  48758