Theorem snsstp1 4792

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 4790	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4153	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3968	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4606	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4008	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3924   ⊆ wss 3926  {csn 4601  {cpr 4603  {ctp 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-pr 4604  df-tp 4606

This theorem is referenced by:  fr3nr  7764  rngbase  17311  srngbase  17322  lmodbase  17338  ipsbase  17349  ipssca  17352  phlbase  17359  topgrpbas  17374  otpsbas  17389  odrngbas  17416  odrngtset  17419  prdssca  17468  prdsbas  17469  prdstset  17478  imasbas  17524  imassca  17531  imastset  17534  fucbas  17974  setcbas  18089  catcbas  18112  estrcbas  18135  cnfldbas  21317  cnfldtset  21323  cnfldbasOLD  21332  cnfldtsetOLD  21336  psrbas  21891  psrsca  21905  trkgbas  28370  rlocbas  33208  rlocaddval  33209  rlocmulval  33210  idlsrgbas  33465  signswch  34539  algbase  43145  clsk1indlem4  44015  clsk1indlem1  44016  cycl3grtri  47907  rngcbasALTV  48189  ringcbasALTV  48223  catbas  49094  mndtcbasval  49405