Theorem snsspr1 4285

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

Syntax hints:   ∪ cun 3538   ⊆ wss 3540  {csn 4125  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-pr 4128

This theorem is referenced by:  snsstp1  4287  op1stb  4867  uniop  4902  rankopb  8598  ltrelxr  9978  2strbas  15810  2strbas1  15813  phlvsca  15861  prdshom  15950  ipobas  16978  ipolerval  16979  lspprid1  18818  lsppratlem3  18970  lsppratlem4  18971  constr3pthlem1  26183  ex-dif  26672  ex-un  26673  ex-in  26674  coinflippv  29872  subfacp1lem2a  30416  altopthsn  31238  rankaltopb  31256  dvh3dim3N  35756  mapdindp2  36028  lspindp5  36077  algsca  36770  clsk1indlem2  37360  clsk1indlem3  37361  clsk1indlem1  37363  gsumpr  41932