Theorem snsspr1 4758

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

Syntax hints:   ∪ cun 3888   ⊆ wss 3890  {csn 4568  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-pr 4571

This theorem is referenced by:  snsstp1  4760  op1stb  5420  uniop  5464  1sdom2dom  9158  rankopb  9770  ltrelxr  11200  seqexw  13973  2strbas  17192  phlvsca  17307  prdshom  17424  ipobas  18491  ipolerval  18492  chnccat  18586  gsumpr  19924  lspprid1  20986  lsppratlem3  21142  lsppratlem4  21143  ex-dif  30511  ex-un  30512  ex-in  30513  idlsrgtset  33586  esplyind  33737  coinflippv  34647  pthhashvtx  35329  subfacp1lem2a  35381  altopthsn  36162  rankaltopb  36180  dvh3dim3N  41912  mapdindp2  42184  lspindp5  42233  algsca  43626  clsk1indlem2  44490  clsk1indlem3  44491  clsk1indlem1  44493  mnuprdlem4  44723  setc1onsubc  50092