Theorem snsspr1 4772

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

Syntax hints:   ∪ cun 3902   ⊆ wss 3904  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-pr 4585

This theorem is referenced by:  snsstp1  4774  op1stb  5439  uniop  5484  1sdom2dom  9198  rankopb  9810  ltrelxr  11243  seqexw  14030  2strbas  17264  phlvsca  17379  prdshom  17496  ipobas  18563  ipolerval  18564  chnccat  18658  gsumpr  19995  lspprid1  21061  lsppratlem3  21216  lsppratlem4  21217  ex-dif  30622  ex-un  30623  ex-in  30624  idlsrgtset  33701  esplyind  33869  coinflippv  34778  pthhashvtx  35475  subfacp1lem2a  35527  altopthsn  36308  rankaltopb  36326  dvh3dim3N  42070  mapdindp2  42342  lspindp5  42391  algsca  43751  clsk1indlem2  44615  clsk1indlem3  44616  clsk1indlem1  44618  mnuprdlem4  44848  setc1onsubc  50220