Theorem snsspr1 4707

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

Syntax hints:   ∪ cun 3879   ⊆ wss 3881  {csn 4525  {cpr 4527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-pr 4528

This theorem is referenced by:  snsstp1  4709  op1stb  5328  uniop  5370  rankopb  9265  ltrelxr  10691  seqexw  13380  2strbas  16595  2strbas1  16598  phlvsca  16649  prdshom  16732  ipobas  17757  ipolerval  17758  gsumpr  19068  lspprid1  19762  lsppratlem3  19914  lsppratlem4  19915  ex-dif  28208  ex-un  28209  ex-in  28210  idlsrgtset  31061  coinflippv  31851  pthhashvtx  32487  subfacp1lem2a  32540  altopthsn  33535  rankaltopb  33553  dvh3dim3N  38745  mapdindp2  39017  lspindp5  39066  algsca  40125  clsk1indlem2  40745  clsk1indlem3  40746  clsk1indlem1  40748  mnuprdlem4  40983