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 4141	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3956	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4594	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3996	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3912   ⊆ wss 3914  {csn 4589  {cpr 4591  {ctp 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-pr 4592  df-tp 4594

This theorem is referenced by:  fr3nr  7748  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  17475  imassca  17482  imastset  17485  fucbas  17925  setcbas  18040  catcbas  18063  estrcbas  18086  cnfldbas  21268  cnfldtset  21274  cnfldbasOLD  21283  cnfldtsetOLD  21287  psrbas  21842  psrsca  21856  trkgbas  28372  rlocbas  33218  rlocaddval  33219  rlocmulval  33220  idlsrgbas  33475  signswch  34552  algbase  43163  clsk1indlem4  44033  clsk1indlem1  44034  cycl3grtri  47946  rngcbasALTV  48254  ringcbasALTV  48288  catbas  49215  mndtcbasval  49569