Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  snsspr1 Structured version   Visualization version   GIF version

Theorem snsspr1 4730
 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
StepHypRef Expression
1 ssun1 4132 . 2 {𝐴} ⊆ ({𝐴} ∪ {𝐵})
2 df-pr 4551 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
31, 2sseqtrri 3988 1 {𝐴} ⊆ {𝐴, 𝐵}
 Colors of variables: wff setvar class Syntax hints:   ∪ cun 3916   ⊆ wss 3918  {csn 4548  {cpr 4550 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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3481  df-un 3923  df-in 3925  df-ss 3935  df-pr 4551 This theorem is referenced by:  snsstp1  4732  op1stb  5346  uniop  5388  rankopb  9267  ltrelxr  10689  seqexw  13380  2strbas  16594  2strbas1  16597  phlvsca  16648  prdshom  16731  ipobas  17756  ipolerval  17757  gsumpr  19066  lspprid1  19757  lsppratlem3  19909  lsppratlem4  19910  ex-dif  28199  ex-un  28200  ex-in  28201  coinflippv  31761  pthhashvtx  32394  subfacp1lem2a  32447  altopthsn  33442  rankaltopb  33460  dvh3dim3N  38650  mapdindp2  38922  lspindp5  38971  algsca  39972  clsk1indlem2  40595  clsk1indlem3  40596  clsk1indlem1  40598  mnuprdlem4  40834
 Copyright terms: Public domain W3C validator