Theorem snsstp1 4783

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 4781	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4144	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3959	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4597	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3999	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3915   ⊆ wss 3917  {csn 4592  {cpr 4594  {ctp 4596

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-pr 4595  df-tp 4597

This theorem is referenced by:  fr3nr  7751  rngbase  17269  srngbase  17280  lmodbase  17296  ipsbase  17307  ipssca  17310  phlbase  17317  topgrpbas  17332  otpsbas  17347  odrngbas  17374  odrngtset  17377  prdssca  17426  prdsbas  17427  prdstset  17436  imasbas  17482  imassca  17489  imastset  17492  fucbas  17932  setcbas  18047  catcbas  18070  estrcbas  18093  cnfldbas  21275  cnfldtset  21281  cnfldbasOLD  21290  cnfldtsetOLD  21294  psrbas  21849  psrsca  21863  trkgbas  28379  rlocbas  33225  rlocaddval  33226  rlocmulval  33227  idlsrgbas  33482  signswch  34559  algbase  43170  clsk1indlem4  44040  clsk1indlem1  44041  cycl3grtri  47950  rngcbasALTV  48258  ringcbasALTV  48292  catbas  49219  mndtcbasval  49573