Theorem snsspr1 4775

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 4124	. 2 ⊢ {𝐴} ⊆ ({𝐴} ∪ {𝐵})
2		df-pr 4587	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3	1, 2	sseqtrri 3980	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵}

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899  {csn 4584  {cpr 4586

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-pr 4587

This theorem is used by:  snsstp1  4777  op1stb  5440  uniop  5488  1sdom2dom  9238  rankopb  9859  ltrelxr  11363  seqexw  14153  2strbas  17399  phlvsca  17514  prdshom  17631  ipobas  18698  ipolerval  18699  chnccat  18793  gsumpr  20162  lspprid1  21265  lsppratlem3  21420  lsppratlem4  21421  pthhashvtx  30308  ex-dif  31017  ex-un  31018  ex-in  31019  idlsrgtset  34033  esplyind  34200  coinflippv  35109  subfacp1lem2a  35924  altopthsn  36706  rankaltopb  36724  dvh3dim3N  42486  mapdindp2  42758  lspindp5  42807  algsca  44163  clsk1indlem2  45027  clsk1indlem3  45028  clsk1indlem1  45030  mnuprdlem4  45244  setc1onsubc  50679