Theorem snsstp1 4746

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 4744	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4102	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3926	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4563	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3954	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4558  {cpr 4560  {ctp 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-pr 4561  df-tp 4563

This theorem is referenced by:  fr3nr  7600  rngbase  16935  srngbase  16946  lmodbase  16962  ipsbase  16972  ipssca  16975  phlbase  16982  topgrpbas  16996  otpsbas  17010  odrngbas  17033  odrngtset  17036  prdssca  17084  prdsbas  17085  prdstset  17094  imasbas  17140  imassca  17147  imastset  17150  fucbas  17593  setcbas  17709  catcbas  17732  estrcbas  17757  cnfldbas  20514  cnfldtset  20518  psrbas  21057  psrsca  21068  trkgbas  26710  idlsrgbas  31551  signswch  32440  algbase  40919  clsk1indlem4  41543  clsk1indlem1  41544  rngcbasALTV  45429  ringcbasALTV  45492  mndtcbasval  46253