Theorem snsspr1 4753

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

Syntax hints:   ∪ cun 3890   ⊆ wss 3892  {csn 4567  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-un 3897  df-in 3899  df-ss 3909  df-pr 4570

This theorem is referenced by:  snsstp1  4755  op1stb  5390  uniop  5433  rankopb  9611  ltrelxr  11037  seqexw  13735  2strbas  16933  2strbas1  16937  phlvsca  17058  prdshom  17176  ipobas  18247  ipolerval  18248  gsumpr  19554  lspprid1  20257  lsppratlem3  20409  lsppratlem4  20410  ex-dif  28783  ex-un  28784  ex-in  28785  idlsrgtset  31649  coinflippv  32446  pthhashvtx  33085  subfacp1lem2a  33138  altopthsn  34259  rankaltopb  34277  dvh3dim3N  39459  mapdindp2  39731  lspindp5  39780  algsca  41003  clsk1indlem2  41622  clsk1indlem3  41623  clsk1indlem1  41625  mnuprdlem4  41863