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  29676  ex-un  29677  ex-in  29678  idlsrgtset  32622  coinflippv  33482  pthhashvtx  34118  subfacp1lem2a  34171  altopthsn  34933  rankaltopb  34951  dvh3dim3N  40320  mapdindp2  40592  lspindp5  40641  algsca  41923  clsk1indlem2  42793  clsk1indlem3  42794  clsk1indlem1  42796  mnuprdlem4  43034