Theorem snsspr1 4818

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

Syntax hints:   ∪ cun 3947   ⊆ wss 3949  {csn 4629  {cpr 4631

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 3954  df-in 3956  df-ss 3966  df-pr 4632

This theorem is referenced by:  snsstp1  4820  op1stb  5472  uniop  5516  1sdom2dom  9247  rankopb  9847  ltrelxr  11275  seqexw  13982  2strbas  17167  2strbas1  17171  phlvsca  17295  prdshom  17413  ipobas  18484  ipolerval  18485  gsumpr  19823  lspprid1  20608  lsppratlem3  20762  lsppratlem4  20763  ex-dif  29707  ex-un  29708  ex-in  29709  idlsrgtset  32653  coinflippv  33513  pthhashvtx  34149  subfacp1lem2a  34202  altopthsn  34964  rankaltopb  34982  dvh3dim3N  40368  mapdindp2  40640  lspindp5  40689  algsca  41971  clsk1indlem2  42841  clsk1indlem3  42842  clsk1indlem1  42844  mnuprdlem4  43082