Theorem snsspr1 4784

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

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {csn 4594  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-pr 4597

This theorem is referenced by:  snsstp1  4786  op1stb  5454  uniop  5499  1sdom2dom  9213  rankopb  9823  ltrelxr  11269  seqexw  14052  2strbas  17287  phlvsca  17402  prdshom  17519  ipobas  18586  ipolerval  18587  chnccat  18681  gsumpr  20024  lspprid1  21095  lsppratlem3  21250  lsppratlem4  21251  ex-dif  30714  ex-un  30715  ex-in  30716  idlsrgtset  33742  esplyind  33909  coinflippv  34818  pthhashvtx  35518  subfacp1lem2a  35570  altopthsn  36351  rankaltopb  36369  dvh3dim3N  42112  mapdindp2  42384  lspindp5  42433  algsca  43795  clsk1indlem2  44659  clsk1indlem3  44660  clsk1indlem1  44662  mnuprdlem4  44876  setc1onsubc  50264