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

Theorem nelsn 4565
 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 4542 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
21necon3ai 3012 1 (𝐴𝐵 → ¬ 𝐴 ∈ {𝐵})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ≠ wne 2987  {csn 4525 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-sn 4526 This theorem is referenced by:  fvunsn  6919  nnoddn2prmb  16143  lbsextlem4  19930  cnfldfunALT  20108  obslbs  20424  logbgcd1irr  25390  upgrres1  27113  cycpmco2  30835  lindssn  31003  submateqlem1  31175  submateqlem2  31176  qqhval2  31348  derangsn  32545  prjspersym  39644  prjspreln0  39646  prjspvs  39647  pr2eldif1  40296  pr2eldif2  40297  clsk3nimkb  40786  clsk1indlem1  40791  disjf1o  41861  cnrefiisplem  42514  fperdvper  42604  dvnmul  42628  wallispi  42755  etransc  42968  gsumge0cl  43053  meadjiunlem  43147  hspmbllem2  43309
 Copyright terms: Public domain W3C validator