Theorem snsstp1 4780

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 4778	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4127	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3943	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4592	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3983	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

This proof depends on syntax axioms:   ∪ cun 3900   ⊆ wss 3902  {csn 4587  {cpr 4589  {ctp 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-pr 4590  df-tp 4592

This theorem is used by:  fr3nr  7774  rngbase  17388  srngbase  17399  lmodbase  17415  ipsbase  17426  ipssca  17429  phlbase  17436  topgrpbas  17451  otpsbas  17466  odrngbas  17493  odrngtset  17496  prdssca  17545  prdsbas  17546  prdstset  17555  imasbas  17602  imassca  17609  imastset  17612  fucbas  18056  setcbas  18171  catcbas  18194  estrcbas  18217  cnfldbas  21590  cnfldtset  21596  psrbas  22150  psrsca  22163  trkgbas  28784  rlocbas  33695  rlocaddval  33696  rlocmulval  33697  idlsrgbas  33901  signswch  35056  algbase  44002  clsk1indlem4  44871  clsk1indlem1  44872  cycl3grtri  48850  rngcbasALTV  49168  ringcbasALTV  49202  catbas  50139  mndtcbasval  50493