Theorem snsstp1 4767

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 4765	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4129	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3945	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4582	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3985	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4577  {cpr 4579  {ctp 4581

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-pr 4580  df-tp 4582

This theorem is referenced by:  fr3nr  7708  rngbase  17203  srngbase  17214  lmodbase  17230  ipsbase  17241  ipssca  17244  phlbase  17251  topgrpbas  17266  otpsbas  17281  odrngbas  17308  odrngtset  17311  prdssca  17360  prdsbas  17361  prdstset  17370  imasbas  17416  imassca  17423  imastset  17426  fucbas  17870  setcbas  17985  catcbas  18008  estrcbas  18031  cnfldbas  21265  cnfldtset  21271  cnfldbasOLD  21280  cnfldtsetOLD  21284  psrbas  21840  psrsca  21854  trkgbas  28390  rlocbas  33208  rlocaddval  33209  rlocmulval  33210  idlsrgbas  33442  signswch  34535  algbase  43157  clsk1indlem4  44027  clsk1indlem1  44028  cycl3grtri  47941  rngcbasALTV  48260  ringcbasALTV  48294  catbas  49221  mndtcbasval  49575