Theorem snsspr1 4817

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

Syntax hints:   ∪ cun 3946   ⊆ wss 3948  {csn 4628  {cpr 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-in 3955  df-ss 3965  df-pr 4631

This theorem is referenced by:  snsstp1  4819  op1stb  5471  uniop  5515  1sdom2dom  9244  rankopb  9844  ltrelxr  11272  seqexw  13979  2strbas  17164  2strbas1  17168  phlvsca  17292  prdshom  17410  ipobas  18481  ipolerval  18482  gsumpr  19818  lspprid1  20601  lsppratlem3  20755  lsppratlem4  20756  ex-dif  29666  ex-un  29667  ex-in  29668  idlsrgtset  32611  coinflippv  33471  pthhashvtx  34107  subfacp1lem2a  34160  altopthsn  34922  rankaltopb  34940  dvh3dim3N  40309  mapdindp2  40581  lspindp5  40630  algsca  41909  clsk1indlem2  42779  clsk1indlem3  42780  clsk1indlem1  42782  mnuprdlem4  43020