Theorem snsstp1 4773

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

Syntax hints:   ∪ cun 3900   ⊆ wss 3902  {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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-ss 3919  df-pr 4584  df-tp 4586

This theorem is referenced by:  fr3nr  7719  rngbase  17223  srngbase  17234  lmodbase  17250  ipsbase  17261  ipssca  17264  phlbase  17271  topgrpbas  17286  otpsbas  17301  odrngbas  17328  odrngtset  17331  prdssca  17380  prdsbas  17381  prdstset  17390  imasbas  17437  imassca  17444  imastset  17447  fucbas  17891  setcbas  18006  catcbas  18029  estrcbas  18052  cnfldbas  21317  cnfldtset  21323  cnfldbasOLD  21332  cnfldtsetOLD  21336  psrbas  21893  psrsca  21907  trkgbas  28521  rlocbas  33351  rlocaddval  33352  rlocmulval  33353  idlsrgbas  33587  signswch  34720  algbase  43483  clsk1indlem4  44352  clsk1indlem1  44353  cycl3grtri  48260  rngcbasALTV  48579  ringcbasALTV  48613  catbas  49538  mndtcbasval  49892