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

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152  {csn 4588  {cpr 4590

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-pr 4591

This theorem is used by:  snsstp1  4777  op1stb  5447  uniop  5495  1sdom2dom  9283  rankopb  9903  ltrelxr  11409  seqexw  14200  2strbas  17450  phlvsca  17567  prdshom  17688  ipobas  18755  ipolerval  18756  chnccat  18850  gsumpr  20220  lspprid1  21323  lsppratlem3  21478  lsppratlem4  21479  cnfldunif  21742  pthhashvtx  30372  ex-dif  31081  ex-un  31082  ex-in  31083  idlsrgtset  34144  esplyind  34318  coinflippv  35227  subfacp1lem2a  36153  altopthsn  36941  rankaltopb  36959  dvh3dim3N  42772  mapdindp2  43044  lspindp5  43093  algsca  44440  clsk1indlem2  45303  clsk1indlem3  45304  clsk1indlem1  45306  mnuprdlem4  45520  setc1onsubc  51071