Theorem snsspr1 4782

Description: A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)

Assertion

Ref	Expression
snsspr1	⊢ {𝐴} ⊆ {𝐴, 𝐵}

Proof of Theorem snsspr1

Step	Hyp	Ref	Expression
1		ssun1 4131	. 2 ⊢ {𝐴} ⊆ ({𝐴} ∪ {𝐵})
2		df-pr 4594	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3	1, 2	sseqtrri 3987	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵}

This proof depends on syntax axioms:   ∪ cun 3904   ⊆ wss 3906  {csn 4591  {cpr 4593

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-pr 4594

This theorem is used by:  snsstp1  4784  op1stb  5455  uniop  5500  1sdom2dom  9221  rankopb  9831  ltrelxr  11285  seqexw  14071  2strbas  17310  phlvsca  17425  prdshom  17542  ipobas  18609  ipolerval  18610  chnccat  18704  gsumpr  20069  lspprid1  21168  lsppratlem3  21323  lsppratlem4  21324  pthhashvtx  30142  ex-dif  30845  ex-un  30846  ex-in  30847  idlsrgtset  33862  esplyind  34029  coinflippv  34939  subfacp1lem2a  35709  altopthsn  36490  rankaltopb  36508  dvh3dim3N  42281  mapdindp2  42553  lspindp5  42602  algsca  43962  clsk1indlem2  44826  clsk1indlem3  44827  clsk1indlem1  44829  mnuprdlem4  45043  setc1onsubc  50437