Theorem snsspr1 4781

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

Syntax hints:   ∪ cun 3915   ⊆ wss 3917  {csn 4592  {cpr 4594

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-pr 4595

This theorem is referenced by:  snsstp1  4783  op1stb  5434  uniop  5478  1sdom2dom  9201  rankopb  9812  ltrelxr  11242  seqexw  13989  2strbas  17205  phlvsca  17320  prdshom  17437  ipobas  18497  ipolerval  18498  gsumpr  19892  lspprid1  20910  lsppratlem3  21066  lsppratlem4  21067  ex-dif  30359  ex-un  30360  ex-in  30361  idlsrgtset  33486  coinflippv  34482  pthhashvtx  35122  subfacp1lem2a  35174  altopthsn  35956  rankaltopb  35974  dvh3dim3N  41450  mapdindp2  41722  lspindp5  41771  algsca  43173  clsk1indlem2  44038  clsk1indlem3  44039  clsk1indlem1  44041  mnuprdlem4  44271  setc1onsubc  49595