Theorem snsspr1 4839

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

Syntax hints:   ∪ cun 3974   ⊆ wss 3976  {csn 4648  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-pr 4651

This theorem is referenced by:  snsstp1  4841  op1stb  5491  uniop  5534  1sdom2dom  9310  rankopb  9921  ltrelxr  11351  seqexw  14068  2strbas  17281  2strbas1  17285  phlvsca  17409  prdshom  17527  ipobas  18601  ipolerval  18602  gsumpr  19997  lspprid1  21018  lsppratlem3  21174  lsppratlem4  21175  ex-dif  30455  ex-un  30456  ex-in  30457  idlsrgtset  33501  coinflippv  34448  pthhashvtx  35095  subfacp1lem2a  35148  altopthsn  35925  rankaltopb  35943  dvh3dim3N  41406  mapdindp2  41678  lspindp5  41727  algsca  43138  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem1  44007  mnuprdlem4  44244