Theorem snsspr1 4752

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

Syntax hints:   ∪ cun 3889   ⊆ wss 3891  {csn 4566  {cpr 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-in 3898  df-ss 3908  df-pr 4569

This theorem is referenced by:  snsstp1  4754  op1stb  5388  uniop  5431  rankopb  9594  ltrelxr  11020  seqexw  13718  2strbas  16916  2strbas1  16920  phlvsca  17041  prdshom  17159  ipobas  18230  ipolerval  18231  gsumpr  19537  lspprid1  20240  lsppratlem3  20392  lsppratlem4  20393  ex-dif  28766  ex-un  28767  ex-in  28768  idlsrgtset  31632  coinflippv  32429  pthhashvtx  33068  subfacp1lem2a  33121  altopthsn  34242  rankaltopb  34260  dvh3dim3N  39442  mapdindp2  39714  lspindp5  39763  algsca  40986  clsk1indlem2  41605  clsk1indlem3  41606  clsk1indlem1  41608  mnuprdlem4  41846