Theorem snsstp1 4759

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 4757	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4118	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3931	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4572	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3971	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3887   ⊆ wss 3889  {csn 4567  {cpr 4569  {ctp 4571

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-pr 4570  df-tp 4572

This theorem is referenced by:  fr3nr  7726  rngbase  17262  srngbase  17273  lmodbase  17289  ipsbase  17300  ipssca  17303  phlbase  17310  topgrpbas  17325  otpsbas  17340  odrngbas  17367  odrngtset  17370  prdssca  17419  prdsbas  17420  prdstset  17429  imasbas  17476  imassca  17483  imastset  17486  fucbas  17930  setcbas  18045  catcbas  18068  estrcbas  18091  cnfldbas  21356  cnfldtset  21362  psrbas  21913  psrsca  21926  trkgbas  28513  rlocbas  33328  rlocaddval  33329  rlocmulval  33330  idlsrgbas  33564  signswch  34705  algbase  43602  clsk1indlem4  44471  clsk1indlem1  44472  cycl3grtri  48423  rngcbasALTV  48742  ringcbasALTV  48776  catbas  49701  mndtcbasval  50055