Theorem snsspr1 4778

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

Syntax hints:   ∪ cun 3912   ⊆ wss 3914  {csn 4589  {cpr 4591

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-pr 4592

This theorem is referenced by:  snsstp1  4780  op1stb  5431  uniop  5475  1sdom2dom  9194  rankopb  9805  ltrelxr  11235  seqexw  13982  2strbas  17198  phlvsca  17313  prdshom  17430  ipobas  18490  ipolerval  18491  gsumpr  19885  lspprid1  20903  lsppratlem3  21059  lsppratlem4  21060  ex-dif  30352  ex-un  30353  ex-in  30354  idlsrgtset  33479  coinflippv  34475  pthhashvtx  35115  subfacp1lem2a  35167  altopthsn  35949  rankaltopb  35967  dvh3dim3N  41443  mapdindp2  41715  lspindp5  41764  algsca  43166  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem1  44034  mnuprdlem4  44264  setc1onsubc  49591