Theorem snsspr1 4819

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

Syntax hints:   ∪ cun 3961   ⊆ wss 3963  {csn 4631  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-pr 4634

This theorem is referenced by:  snsstp1  4821  op1stb  5482  uniop  5525  1sdom2dom  9281  rankopb  9890  ltrelxr  11320  seqexw  14055  2strbas  17268  2strbas1  17272  phlvsca  17396  prdshom  17514  ipobas  18589  ipolerval  18590  gsumpr  19988  lspprid1  21013  lsppratlem3  21169  lsppratlem4  21170  ex-dif  30452  ex-un  30453  ex-in  30454  idlsrgtset  33516  coinflippv  34465  pthhashvtx  35112  subfacp1lem2a  35165  altopthsn  35943  rankaltopb  35961  dvh3dim3N  41432  mapdindp2  41704  lspindp5  41753  algsca  43166  clsk1indlem2  44032  clsk1indlem3  44033  clsk1indlem1  44035  mnuprdlem4  44271