Theorem snsspr1 4780

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

Syntax hints:   ∪ cun 3903   ⊆ wss 3905  {csn 4589  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-pr 4592

This theorem is referenced by:  snsstp1  4782  op1stb  5453  uniop  5498  1sdom2dom  9210  rankopb  9820  ltrelxr  11265  seqexw  14049  2strbas  17283  phlvsca  17398  prdshom  17515  ipobas  18582  ipolerval  18583  chnccat  18677  gsumpr  20020  lspprid1  21118  lsppratlem3  21273  lsppratlem4  21274  ex-dif  30774  ex-un  30775  ex-in  30776  idlsrgtset  33798  esplyind  33965  coinflippv  34874  pthhashvtx  35620  subfacp1lem2a  35672  altopthsn  36453  rankaltopb  36471  dvh3dim3N  42223  mapdindp2  42495  lspindp5  42544  algsca  43904  clsk1indlem2  44768  clsk1indlem3  44769  clsk1indlem1  44771  mnuprdlem4  44985  setc1onsubc  50380