Theorem snsstp1 4750

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

Syntax hints:   ∪ cun 3883   ⊆ wss 3885  {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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-un 3890  df-ss 3902  df-pr 4561  df-tp 4563

This theorem is referenced by:  fr3nr  7719  rngbase  17257  srngbase  17268  lmodbase  17284  ipsbase  17295  ipssca  17298  phlbase  17305  topgrpbas  17320  otpsbas  17335  odrngbas  17362  odrngtset  17365  prdssca  17414  prdsbas  17415  prdstset  17424  imasbas  17471  imassca  17478  imastset  17481  fucbas  17925  setcbas  18040  catcbas  18063  estrcbas  18086  cnfldbas  21355  cnfldtset  21361  psrbas  21913  psrsca  21926  trkgbas  28535  rlocbas  33352  rlocaddval  33353  rlocmulval  33354  idlsrgbas  33599  signswch  34757  algbase  43634  clsk1indlem4  44503  clsk1indlem1  44504  cycl3grtri  48452  rngcbasALTV  48771  ringcbasALTV  48805  catbas  49730  mndtcbasval  50084