Theorem nelsn 4627

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

Step	Hyp	Ref	Expression
1		elsni 4601	. 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2	1	necon3ai 2981	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵})

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ≠ wne 2956  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-sn 4585

This theorem is used by:  frd  5608  fvn0fvelrn  6912  fvunsn  7182  fzdif1  13732  nnoddn2prmb  16984  chnccat  18793  drnglidl1ne0  20762  isdrng3lem2  20999  lbsextlem4  21432  cnfldfun  21685  obslbs  22029  logbgcd1irr  27115  upgrres1  29887  cycpmco2  33687  elrgspnlem4  33799  lindssn  33926  drngidlhash  33976  drng0mxidl  33993  rsprprmprmidlb  34048  rprmirredb  34057  1arithufdlem4  34072  ig1pmindeg  34127  irngnminplynz  34337  algextdeglem4  34345  submateqlem1  34432  submateqlem2  34433  qqhval2  34607  derangsn  35914  ricdrng1  43572  prjspersym  43615  prjspreln0  43617  prjspnvs  43628  pr2eldif1  44539  pr2eldif2  44540  clsk3nimkb  45025  clsk1indlem1  45030  disjf1o  46175  cnrefiisplem  46808  fperdvper  46898  dvnmul  46922  wallispi  47049  etransc  47262  gsumge0cl  47350  meadjiunlem  47444  hspmbllem2  47606  numtowerdt  47885