Theorem snsspr1 4745

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

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4555  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-pr 4558

This theorem is referenced by:  snsstp1  4747  op1stb  5411  uniop  5456  1sdom2dom  9154  rankopb  9767  ltrelxr  11197  seqexw  13970  2strbas  17189  phlvsca  17304  prdshom  17421  ipobas  18488  ipolerval  18489  chnccat  18583  gsumpr  19921  lspprid1  20987  lsppratlem3  21142  lsppratlem4  21143  ex-dif  30511  ex-un  30512  ex-in  30513  idlsrgtset  33591  esplyind  33759  coinflippv  34668  pthhashvtx  35356  subfacp1lem2a  35408  altopthsn  36189  rankaltopb  36207  dvh3dim3N  41941  mapdindp2  42213  lspindp5  42262  algsca  43622  clsk1indlem2  44486  clsk1indlem3  44487  clsk1indlem1  44489  mnuprdlem4  44719  setc1onsubc  50092