Theorem snsspr1 4768

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

Syntax hints:   ∪ cun 3897   ⊆ wss 3899  {csn 4578  {cpr 4580

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-pr 4581

This theorem is referenced by:  snsstp1  4770  op1stb  5417  uniop  5461  1sdom2dom  9152  rankopb  9762  ltrelxr  11191  seqexw  13938  2strbas  17153  phlvsca  17268  prdshom  17385  ipobas  18452  ipolerval  18453  chnccat  18547  gsumpr  19882  lspprid1  20946  lsppratlem3  21102  lsppratlem4  21103  ex-dif  30447  ex-un  30448  ex-in  30449  idlsrgtset  33538  esplyind  33680  coinflippv  34590  pthhashvtx  35271  subfacp1lem2a  35323  altopthsn  36104  rankaltopb  36122  dvh3dim3N  41648  mapdindp2  41920  lspindp5  41969  algsca  43361  clsk1indlem2  44225  clsk1indlem3  44226  clsk1indlem1  44228  mnuprdlem4  44458  setc1onsubc  49789