Theorem snsstp1 4287

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 4285	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 3738	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3577	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4130	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtr4i 3601	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3538   ⊆ wss 3540  {csn 4125  {cpr 4127  {ctp 4129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-pr 4128  df-tp 4130

This theorem is referenced by:  fr3nr  6871  rngbase  15824  srngbase  15832  lmodbase  15841  ipsbase  15848  ipssca  15851  phlbase  15858  topgrpbas  15866  otpsbas  15875  otpsbasOLD  15879  odrngbas  15890  odrngtset  15893  prdssca  15939  prdsbas  15940  prdstset  15949  imasbas  15995  imassca  16002  imastset  16005  fucbas  16443  setcbas  16551  catcbas  16570  estrcbas  16588  xpcbas  16641  psrbas  19199  psrsca  19210  cnfldbas  19571  cnfldtset  19575  trkgbas  25144  signswch  29964  algbase  36767  clsk1indlem4  37362  clsk1indlem1  37363  rngcbasALTV  41775  ringcbasALTV  41838