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

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897  df-in 3899  df-ss 3909  df-pr 4568

This theorem is referenced by:  snsstp1  4755  op1stb  5399  uniop  5442  1sdom2dom  9068  rankopb  9658  ltrelxr  11086  seqexw  13787  2strbas  16984  2strbas1  16988  phlvsca  17109  prdshom  17227  ipobas  18298  ipolerval  18299  gsumpr  19605  lspprid1  20308  lsppratlem3  20460  lsppratlem4  20461  ex-dif  28836  ex-un  28837  ex-in  28838  idlsrgtset  31702  coinflippv  32499  pthhashvtx  33138  subfacp1lem2a  33191  altopthsn  34312  rankaltopb  34330  dvh3dim3N  39663  mapdindp2  39935  lspindp5  39984  algsca  41202  clsk1indlem2  41865  clsk1indlem3  41866  clsk1indlem1  41868  mnuprdlem4  42106