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 4123	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3939	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4588	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3979	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

This proof depends on syntax axioms:   ∪ cun 3896   ⊆ wss 3898  {csn 4583  {cpr 4585  {ctp 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3903  df-ss 3915  df-pr 4586  df-tp 4588

This theorem is used by:  fr3nr  7769  rngbase  17431  srngbase  17442  lmodbase  17458  ipsbase  17469  ipssca  17472  phlbase  17479  topgrpbas  17494  otpsbas  17509  odrngbas  17536  odrngtset  17539  prdssca  17588  prdsbas  17589  prdstset  17598  imasbas  17645  imassca  17652  imastset  17655  fucbas  18099  setcbas  18214  catcbas  18237  estrcbas  18260  cnfldbas  21643  cnfldtset  21649  psrbas  22203  psrsca  22216  trkgbas  28840  angmgmlem  29328  angmgmbas  29331  rlocbas  33762  rlocaddval  33763  rlocmulval  33764  idlsrgbas  33969  signswch  35124  algbase  44119  clsk1indlem4  44988  clsk1indlem1  44989  cycl3grtri  48967  rngcbasALTV  49285  ringcbasALTV  49319  catbas  50256  mndtcbasval  50610