Theorem snsstp2 4288

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 4286	. . 3 ⊢ {𝐵} ⊆ {𝐴, 𝐵}
2		ssun1 3738	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3577	. 2 ⊢ {𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4130	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtr4i 3601	1 ⊢ {𝐵} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3538   ⊆ wss 3540  {csn 4125  {cpr 4127  {ctp 4129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-pr 4128  df-tp 4130

This theorem is referenced by:  fr3nr  6871  rngplusg  15825  srngplusg  15833  lmodplusg  15842  ipsaddg  15849  ipsvsca  15852  phlplusg  15859  topgrpplusg  15867  otpstset  15876  otpstsetOLD  15880  odrngplusg  15891  odrngle  15894  prdsplusg  15941  prdsvsca  15943  prdsle  15945  imasplusg  16000  imasvsca  16003  imasle  16006  fuchom  16444  setchomfval  16552  catchomfval  16571  estrchomfval  16589  xpchomfval  16642  psrplusg  19202  psrvscafval  19211  cnfldadd  19572  cnfldle  19576  trkgdist  25145  algaddg  36768  clsk1indlem4  37362  rngchomfvalALTV  41776  ringchomfvalALTV  41839