Theorem snsstp2 4624

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 4622	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 4038	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3868	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4446	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtr4i 3895	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3828   ⊆ wss 3830  {csn 4441  {cpr 4443  {ctp 4445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-v 3418  df-un 3835  df-in 3837  df-ss 3844  df-pr 4444  df-tp 4446

This theorem is referenced by:  fr3nr  7310  rngplusg  16477  srngplusg  16485  lmodplusg  16494  ipsaddg  16501  ipsvsca  16504  phlplusg  16511  topgrpplusg  16519  otpstset  16526  odrngplusg  16537  odrngle  16540  prdsplusg  16587  prdsvsca  16589  prdsle  16591  imasplusg  16646  imasvsca  16649  imasle  16652  fuchom  17089  setchomfval  17197  catchomfval  17216  estrchomfval  17234  xpchomfval  17287  psrplusg  19875  psrvscafval  19884  cnfldadd  20252  cnfldle  20256  trkgdist  25934  algaddg  39172  clsk1indlem4  39754  rngchomfvalALTV  43617  ringchomfvalALTV  43680