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

Theorem nelsn 4510
 Description: If a class is not equal to the class in a singleton, then it is not in the singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.) (Proof shortened by BJ, 4-May-2021.)
Assertion
Ref Expression
nelsn (𝐴𝐵 → ¬ 𝐴 ∈ {𝐵})

Proof of Theorem nelsn
StepHypRef Expression
1 elsni 4489 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
21necon3ai 3009 1 (𝐴𝐵 → ¬ 𝐴 ∈ {𝐵})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2081   ≠ wne 2984  {csn 4472 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-sn 4473 This theorem is referenced by:  fvunsn  6804  nnoddn2prmb  15979  lbsextlem4  19623  cnfldfunALT  20240  obslbs  20556  logbgcd1irr  25053  upgrres1  26778  lindssn  30585  submateqlem1  30687  submateqlem2  30688  qqhval2  30840  derangsn  32025  prjspersym  38754  prjspreln0  38756  prjspvs  38757  pr2eldif1  39398  pr2eldif2  39399  clsk3nimkb  39875  clsk1indlem1  39880  disjf1o  40992  cnrefiisplem  41652  fperdvper  41744  dvnmul  41769  wallispi  41897  etransc  42110  gsumge0cl  42195  meadjiunlem  42289  hspmbllem2  42451
 Copyright terms: Public domain W3C validator