Theorem snsstp1 4820

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 4818	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4187	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 4004	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4635	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4032	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3960   ⊆ wss 3962  {csn 4630  {cpr 4632  {ctp 4634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-pr 4633  df-tp 4635

This theorem is referenced by:  fr3nr  7790  rngbase  17344  srngbase  17355  lmodbase  17371  ipsbase  17382  ipssca  17385  phlbase  17392  topgrpbas  17407  otpsbas  17422  odrngbas  17449  odrngtset  17452  prdssca  17502  prdsbas  17503  prdstset  17512  imasbas  17558  imassca  17565  imastset  17568  fucbas  18015  setcbas  18131  catcbas  18154  estrcbas  18179  cnfldbas  21385  cnfldtset  21391  cnfldbasOLD  21400  cnfldtsetOLD  21404  psrbas  21970  psrsca  21984  trkgbas  28467  rlocbas  33253  rlocaddval  33254  rlocmulval  33255  idlsrgbas  33511  signswch  34554  algbase  43162  clsk1indlem4  44033  clsk1indlem1  44034  rngcbasALTV  48109  ringcbasALTV  48143  mndtcbasval  48888