Theorem snsstp1 4749

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 4747	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4106	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3930	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4566	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3958	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3885   ⊆ wss 3887  {csn 4561  {cpr 4563  {ctp 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-pr 4564  df-tp 4566

This theorem is referenced by:  fr3nr  7622  rngbase  17009  srngbase  17020  lmodbase  17036  ipsbase  17047  ipssca  17050  phlbase  17057  topgrpbas  17072  otpsbas  17087  odrngbas  17114  odrngtset  17117  prdssca  17167  prdsbas  17168  prdstset  17177  imasbas  17223  imassca  17230  imastset  17233  fucbas  17677  setcbas  17793  catcbas  17816  estrcbas  17841  cnfldbas  20601  cnfldtset  20605  psrbas  21147  psrsca  21158  trkgbas  26806  idlsrgbas  31649  signswch  32540  algbase  41003  clsk1indlem4  41654  clsk1indlem1  41655  rngcbasALTV  45541  ringcbasALTV  45604  mndtcbasval  46367