Theorem snsspr1 4765

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

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4577  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-pr 4580

This theorem is referenced by:  snsstp1  4767  op1stb  5414  uniop  5458  1sdom2dom  9143  rankopb  9748  ltrelxr  11176  seqexw  13924  2strbas  17139  phlvsca  17254  prdshom  17371  ipobas  18437  ipolerval  18438  gsumpr  19834  lspprid1  20900  lsppratlem3  21056  lsppratlem4  21057  ex-dif  30367  ex-un  30368  ex-in  30369  idlsrgtset  33445  coinflippv  34452  pthhashvtx  35101  subfacp1lem2a  35153  altopthsn  35935  rankaltopb  35953  dvh3dim3N  41428  mapdindp2  41700  lspindp5  41749  algsca  43150  clsk1indlem2  44015  clsk1indlem3  44016  clsk1indlem1  44018  mnuprdlem4  44248  setc1onsubc  49587