Theorem snsspr1 4770

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

Syntax hints:   ∪ cun 3899   ⊆ wss 3901  {csn 4580  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-pr 4583

This theorem is referenced by:  snsstp1  4772  op1stb  5419  uniop  5463  1sdom2dom  9154  rankopb  9764  ltrelxr  11193  seqexw  13940  2strbas  17155  phlvsca  17270  prdshom  17387  ipobas  18454  ipolerval  18455  chnccat  18549  gsumpr  19884  lspprid1  20948  lsppratlem3  21104  lsppratlem4  21105  ex-dif  30498  ex-un  30499  ex-in  30500  idlsrgtset  33589  esplyind  33731  coinflippv  34641  pthhashvtx  35322  subfacp1lem2a  35374  altopthsn  36155  rankaltopb  36173  dvh3dim3N  41709  mapdindp2  41981  lspindp5  42030  algsca  43419  clsk1indlem2  44283  clsk1indlem3  44284  clsk1indlem1  44286  mnuprdlem4  44516  setc1onsubc  49847