Theorem nelsn 4628

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 2984	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵})

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2147   ≠ wne 2959  {csn 4588

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-sn 4589

This theorem is used by:  frd  5615  fvn0fvelrn  6945  fvunsn  7215  fzdif1  13779  nnoddn2prmb  17035  chnccat  18850  drnglidl1ne0  20820  isdrng3lem2  21057  lbsextlem4  21490  cnfldfun  21744  obslbs  22091  logbgcd1irr  27179  upgrres1  29951  cycpmco2  33793  elrgspnlem4  33905  lindssn  34037  drngidlhash  34087  drng0mxidl  34104  rsprprmprmidlb  34159  rprmirredb  34168  1arithufdlem4  34183  ig1pmindeg  34237  irngnminplynz  34455  algextdeglem4  34463  submateqlem1  34550  submateqlem2  34551  qqhval2  34725  derangsn  36143  ricdrng1  43858  prjspersym  43901  prjspreln0  43903  prjspnvs  43914  pr2eldif1  44816  pr2eldif2  44817  clsk3nimkb  45301  clsk1indlem1  45306  disjf1o  46479  cnrefiisplem  47112  fperdvper  47202  dvnmul  47226  wallispi  47353  etransc  47566  gsumge0cl  47654  meadjiunlem  47748  hspmbllem2  47910  numtowerdt  48189