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

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-pr 4585

This theorem is referenced by:  snsstp1  4774  op1stb  5427  uniop  5471  1sdom2dom  9166  rankopb  9776  ltrelxr  11205  seqexw  13952  2strbas  17167  phlvsca  17282  prdshom  17399  ipobas  18466  ipolerval  18467  chnccat  18561  gsumpr  19896  lspprid1  20960  lsppratlem3  21116  lsppratlem4  21117  ex-dif  30510  ex-un  30511  ex-in  30512  idlsrgtset  33601  esplyind  33752  coinflippv  34662  pthhashvtx  35344  subfacp1lem2a  35396  altopthsn  36177  rankaltopb  36195  dvh3dim3N  41825  mapdindp2  42097  lspindp5  42146  algsca  43534  clsk1indlem2  44398  clsk1indlem3  44399  clsk1indlem1  44401  mnuprdlem4  44631  setc1onsubc  49961