Theorem snsspr1 4787

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

Syntax hints:   ∪ cun 3922   ⊆ wss 3924  {csn 4599  {cpr 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-un 3929  df-ss 3941  df-pr 4602

This theorem is referenced by:  snsstp1  4789  op1stb  5443  uniop  5487  1sdom2dom  9249  rankopb  9858  ltrelxr  11288  seqexw  14024  2strbas  17234  phlvsca  17349  prdshom  17466  ipobas  18526  ipolerval  18527  gsumpr  19921  lspprid1  20939  lsppratlem3  21095  lsppratlem4  21096  ex-dif  30336  ex-un  30337  ex-in  30338  idlsrgtset  33441  coinflippv  34424  pthhashvtx  35071  subfacp1lem2a  35123  altopthsn  35900  rankaltopb  35918  dvh3dim3N  41389  mapdindp2  41661  lspindp5  41710  algsca  43126  clsk1indlem2  43991  clsk1indlem3  43992  clsk1indlem1  43994  mnuprdlem4  44225