Theorem snsstp1 4770

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 4768	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4128	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3941	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4583	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3981	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3897   ⊆ wss 3899  {csn 4578  {cpr 4580  {ctp 4582

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 2115  ax-9 2123  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-pr 4581  df-tp 4583

This theorem is referenced by:  fr3nr  7715  rngbase  17217  srngbase  17228  lmodbase  17244  ipsbase  17255  ipssca  17258  phlbase  17265  topgrpbas  17280  otpsbas  17295  odrngbas  17322  odrngtset  17325  prdssca  17374  prdsbas  17375  prdstset  17384  imasbas  17431  imassca  17438  imastset  17441  fucbas  17885  setcbas  18000  catcbas  18023  estrcbas  18046  cnfldbas  21311  cnfldtset  21317  cnfldbasOLD  21326  cnfldtsetOLD  21330  psrbas  21887  psrsca  21901  trkgbas  28466  rlocbas  33298  rlocaddval  33299  rlocmulval  33300  idlsrgbas  33534  signswch  34667  algbase  43358  clsk1indlem4  44227  clsk1indlem1  44228  cycl3grtri  48135  rngcbasALTV  48454  ringcbasALTV  48488  catbas  49413  mndtcbasval  49767