Theorem snsstp3 4792

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

Syntax hints:   ∪ cun 3922   ⊆ wss 3924  {csn 4599  {cpr 4601  {ctp 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-un 3929  df-ss 3941  df-tp 4604

This theorem is referenced by:  fr3nr  7761  rngmulr  17302  srngmulr  17313  lmodsca  17329  ipsmulr  17340  ipsip  17343  phlsca  17350  topgrptset  17365  otpsle  17380  odrngmulr  17407  odrngds  17410  prdsmulr  17460  prdsip  17462  prdsds  17465  imasds  17514  imasmulr  17519  imasip  17522  fuccofval  17962  setccofval  18082  catccofval  18104  estrccofval  18128  xpccofval  18181  mpocnfldmul  21309  cnfldds  21314  cnfldmulOLD  21323  cnflddsOLD  21327  psrmulr  21889  trkgitv  28360  rlocmulval  33201  idlsrgmulr  33459  signswch  34522  algmulr  43132  clsk1indlem1  44001  rngccofvalALTV  48139  ringccofvalALTV  48173  catcofval  49011  mndtcco  49323