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

Theorem nelsn 4581
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 4558 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
21necon3ai 2965 1 (𝐴𝐵 → ¬ 𝐴 ∈ {𝐵})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2110  wne 2940  {csn 4541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-sn 4542
This theorem is referenced by:  fvunsn  6994  nnoddn2prmb  16366  lbsextlem4  20198  cnfldfunALT  20376  obslbs  20692  logbgcd1irr  25677  upgrres1  27401  cycpmco2  31119  lindssn  31287  submateqlem1  31471  submateqlem2  31472  qqhval2  31644  derangsn  32845  prjspersym  40154  prjspreln0  40156  prjspvs  40157  prjspnvs  40167  pr2eldif1  40837  pr2eldif2  40838  clsk3nimkb  41327  clsk1indlem1  41332  disjf1o  42402  cnrefiisplem  43045  fperdvper  43135  dvnmul  43159  wallispi  43286  etransc  43499  gsumge0cl  43584  meadjiunlem  43678  hspmbllem2  43840
  Copyright terms: Public domain W3C validator