Theorem snsspr1 4781

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

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {csn 4591  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-pr 4594

This theorem is referenced by:  snsstp1  4783  op1stb  5451  uniop  5496  1sdom2dom  9210  rankopb  9820  ltrelxr  11266  seqexw  14049  2strbas  17284  phlvsca  17399  prdshom  17516  ipobas  18583  ipolerval  18584  chnccat  18678  gsumpr  20021  lspprid1  21092  lsppratlem3  21247  lsppratlem4  21248  ex-dif  30711  ex-un  30712  ex-in  30713  idlsrgtset  33739  esplyind  33906  coinflippv  34815  pthhashvtx  35515  subfacp1lem2a  35567  altopthsn  36348  rankaltopb  36366  dvh3dim3N  42108  mapdindp2  42380  lspindp5  42429  algsca  43791  clsk1indlem2  44655  clsk1indlem3  44656  clsk1indlem1  44658  mnuprdlem4  44872  setc1onsubc  50260