Theorem snsspr1 4790

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

Syntax hints:   ∪ cun 3924   ⊆ wss 3926  {csn 4601  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-pr 4604

This theorem is referenced by:  snsstp1  4792  op1stb  5446  uniop  5490  1sdom2dom  9255  rankopb  9866  ltrelxr  11296  seqexw  14035  2strbas  17249  phlvsca  17364  prdshom  17481  ipobas  18541  ipolerval  18542  gsumpr  19936  lspprid1  20954  lsppratlem3  21110  lsppratlem4  21111  ex-dif  30404  ex-un  30405  ex-in  30406  idlsrgtset  33523  coinflippv  34516  pthhashvtx  35150  subfacp1lem2a  35202  altopthsn  35979  rankaltopb  35997  dvh3dim3N  41468  mapdindp2  41740  lspindp5  41789  algsca  43201  clsk1indlem2  44066  clsk1indlem3  44067  clsk1indlem1  44069  mnuprdlem4  44299  setc1onsubc  49479