Theorem snsstp2 4842

Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)

Assertion

Ref	Expression
snsstp2	⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Proof of Theorem snsstp2

Step	Hyp	Ref	Expression
1		snsspr2 4840	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4201	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 4018	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4653	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	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-pr 4651  df-tp 4653

This theorem is referenced by:  fr3nr  7807  rngplusg  17359  srngplusg  17370  lmodplusg  17386  ipsaddg  17397  ipsvsca  17400  phlplusg  17407  topgrpplusg  17422  otpstset  17437  odrngplusg  17464  odrngle  17467  prdsplusg  17518  prdsvsca  17520  prdsle  17522  imasplusg  17577  imasvsca  17580  imasle  17583  fuchom  18030  fuchomOLD  18031  setchomfval  18146  catchomfval  18169  estrchomfval  18194  xpchomfval  18248  mpocnfldadd  21392  cnfldle  21398  cnfldaddOLD  21407  cnfldleOLD  21411  psrplusg  21979  psrvscafval  21991  trkgdist  28472  rlocaddval  33240  idlsrgplusg  33498  algaddg  43136  clsk1indlem4  44006  rngchomfvalALTV  47990  ringchomfvalALTV  48024  mndtchom  48757