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

Theorem nelsn 4597
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 4576 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
21necon3ai 3041 1 (𝐴𝐵 → ¬ 𝐴 ∈ {𝐵})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2105  wne 3016  {csn 4559
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-ne 3017  df-sn 4560
This theorem is referenced by:  fvunsn  6934  nnoddn2prmb  16140  lbsextlem4  19864  cnfldfunALT  20488  obslbs  20804  logbgcd1irr  25299  upgrres1  27023  cycpmco2  30703  lindssn  30867  submateqlem1  30972  submateqlem2  30973  qqhval2  31123  derangsn  32315  prjspersym  39137  prjspreln0  39139  prjspvs  39140  pr2eldif1  39793  pr2eldif2  39794  clsk3nimkb  40270  clsk1indlem1  40275  disjf1o  41332  cnrefiisplem  41990  fperdvper  42083  dvnmul  42108  wallispi  42236  etransc  42449  gsumge0cl  42534  meadjiunlem  42628  hspmbllem2  42790
  Copyright terms: Public domain W3C validator