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

Theorem snsspr1 4741
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 4147 . 2 {𝐴} ⊆ ({𝐴} ∪ {𝐵})
2 df-pr 4562 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
31, 2sseqtrri 4003 1 {𝐴} ⊆ {𝐴, 𝐵}
Colors of variables: wff setvar class
Syntax hints:  cun 3933  wss 3935  {csn 4559  {cpr 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3940  df-in 3942  df-ss 3951  df-pr 4562
This theorem is referenced by:  snsstp1  4743  op1stb  5355  uniop  5397  rankopb  9270  ltrelxr  10691  seqexw  13375  2strbas  16593  2strbas1  16596  phlvsca  16647  prdshom  16730  ipobas  17755  ipolerval  17756  gsumpr  19006  lspprid1  19700  lsppratlem3  19852  lsppratlem4  19853  ex-dif  28130  ex-un  28131  ex-in  28132  coinflippv  31641  pthhashvtx  32272  subfacp1lem2a  32325  altopthsn  33320  rankaltopb  33338  dvh3dim3N  38467  mapdindp2  38739  lspindp5  38788  algsca  39661  clsk1indlem2  40272  clsk1indlem3  40273  clsk1indlem1  40275  mnuprdlem4  40491
  Copyright terms: Public domain W3C validator