Theorem snsstp1 4771

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 4769	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4127	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3948	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4586	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3976	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3903   ⊆ wss 3905  {csn 4581  {cpr 4583  {ctp 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-un 3910  df-in 3912  df-ss 3922  df-pr 4584  df-tp 4586

This theorem is referenced by:  fr3nr  7693  rngbase  17111  srngbase  17122  lmodbase  17138  ipsbase  17149  ipssca  17152  phlbase  17159  topgrpbas  17174  otpsbas  17189  odrngbas  17216  odrngtset  17219  prdssca  17269  prdsbas  17270  prdstset  17279  imasbas  17325  imassca  17332  imastset  17335  fucbas  17779  setcbas  17895  catcbas  17918  estrcbas  17943  cnfldbas  20711  cnfldtset  20715  psrbas  21257  psrsca  21268  trkgbas  27161  idlsrgbas  32010  signswch  32904  algbase  41317  clsk1indlem4  42027  clsk1indlem1  42028  rngcbasALTV  45959  ringcbasALTV  46022  mndtcbasval  46784