Theorem snsstp1 4776

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 4774	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4137	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3953	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4590	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3993	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3909   ⊆ wss 3911  {csn 4585  {cpr 4587  {ctp 4589

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 3446  df-un 3916  df-ss 3928  df-pr 4588  df-tp 4590

This theorem is referenced by:  fr3nr  7728  rngbase  17238  srngbase  17249  lmodbase  17265  ipsbase  17276  ipssca  17279  phlbase  17286  topgrpbas  17301  otpsbas  17316  odrngbas  17343  odrngtset  17346  prdssca  17395  prdsbas  17396  prdstset  17405  imasbas  17451  imassca  17458  imastset  17461  fucbas  17905  setcbas  18020  catcbas  18043  estrcbas  18066  cnfldbas  21300  cnfldtset  21306  cnfldbasOLD  21315  cnfldtsetOLD  21319  psrbas  21875  psrsca  21889  trkgbas  28425  rlocbas  33234  rlocaddval  33235  rlocmulval  33236  idlsrgbas  33468  signswch  34545  algbase  43156  clsk1indlem4  44026  clsk1indlem1  44027  cycl3grtri  47939  rngcbasALTV  48247  ringcbasALTV  48281  catbas  49208  mndtcbasval  49562