Theorem snsstp1 4781

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

This proof depends on syntax axioms:   ∪ cun 3902   ⊆ wss 3904  {csn 4588  {cpr 4590  {ctp 4592

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-pr 4591  df-tp 4593

This theorem is used by:  fr3nr  7769  rngbase  17358  srngbase  17369  lmodbase  17385  ipsbase  17396  ipssca  17399  phlbase  17406  topgrpbas  17421  otpsbas  17436  odrngbas  17463  odrngtset  17466  prdssca  17515  prdsbas  17516  prdstset  17525  imasbas  17572  imassca  17579  imastset  17582  fucbas  18026  setcbas  18141  catcbas  18164  estrcbas  18187  cnfldbas  21537  cnfldtset  21543  psrbas  22095  psrsca  22108  trkgbas  28725  rlocbas  33597  rlocaddval  33598  rlocmulval  33599  idlsrgbas  33803  signswch  34957  algbase  43929  clsk1indlem4  44798  clsk1indlem1  44799  cycl3grtri  48740  rngcbasALTV  49059  ringcbasALTV  49093  catbas  50032  mndtcbasval  50386