Theorem snsstp1 4765

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

Assertion

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

Proof of Theorem snsstp1

Step	Hyp	Ref	Expression
1		snsspr1 4763	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4125	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3939	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4578	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3979	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3895   ⊆ wss 3897  {csn 4573  {cpr 4575  {ctp 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-pr 4576  df-tp 4578

This theorem is referenced by:  fr3nr  7705  rngbase  17203  srngbase  17214  lmodbase  17230  ipsbase  17241  ipssca  17244  phlbase  17251  topgrpbas  17266  otpsbas  17281  odrngbas  17308  odrngtset  17311  prdssca  17360  prdsbas  17361  prdstset  17370  imasbas  17416  imassca  17423  imastset  17426  fucbas  17870  setcbas  17985  catcbas  18008  estrcbas  18031  cnfldbas  21295  cnfldtset  21301  cnfldbasOLD  21310  cnfldtsetOLD  21314  psrbas  21870  psrsca  21884  trkgbas  28423  rlocbas  33234  rlocaddval  33235  rlocmulval  33236  idlsrgbas  33469  signswch  34574  algbase  43266  clsk1indlem4  44136  clsk1indlem1  44137  cycl3grtri  48046  rngcbasALTV  48365  ringcbasALTV  48399  catbas  49326  mndtcbasval  49680