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

This proof depends on syntax axioms:   ⊆ wss 3895   ∪ cun 4149  {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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-pr 4586  df-tp 4588

This theorem is used by:  fr3nr  7786  rngbase  17470  srngbase  17481  lmodbase  17497  ipsbase  17508  ipssca  17511  phlbase  17518  topgrpbas  17533  otpsbas  17548  odrngbas  17575  odrngtset  17578  prdssca  17627  prdsbas  17628  prdstset  17637  imasbas  17684  imassca  17691  imastset  17694  fucbas  18138  setcbas  18253  catcbas  18276  estrcbas  18299  cnfldbas  21682  cnfldtset  21688  psrbas  22242  psrsca  22255  trkgbas  28907  angmgmlem  29395  angmgmbas  29398  rlocbas  33829  rlocaddval  33830  rlocmulval  33831  idlsrgbas  34036  signswch  35190  algbase  44176  clsk1indlem4  45044  clsk1indlem1  45045  cycl3grtri  49045  rngcbasALTV  49363  ringcbasALTV  49397  catbas  50334  mndtcbasval  50688