Theorem nelsn 4625

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 4599	. 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
2	1	necon3ai 2958	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵})

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ≠ wne 2933  {csn 4582

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-sn 4583

This theorem is referenced by:  frd  5589  fvn0fvelrn  6871  fvunsn  7135  fzdif1  13533  nnoddn2prmb  16753  chnccat  18561  lbsextlem4  21128  cnfldfun  21335  cnfldfunOLD  21348  obslbs  21697  logbgcd1irr  26772  upgrres1  29398  cycpmco2  33227  elrgspnlem4  33339  lindssn  33471  drngidlhash  33527  drnglidl1ne0  33568  drng0mxidl  33569  rsprprmprmidlb  33616  rprmirredb  33625  1arithufdlem4  33640  ig1pmindeg  33695  irngnminplynz  33890  algextdeglem4  33898  submateqlem1  33985  submateqlem2  33986  qqhval2  34160  derangsn  35386  ricdrng1  42898  prjspersym  42965  prjspreln0  42967  prjspnvs  42978  pr2eldif1  43910  pr2eldif2  43911  clsk3nimkb  44396  clsk1indlem1  44401  disjf1o  45550  cnrefiisplem  46187  fperdvper  46277  dvnmul  46301  wallispi  46428  etransc  46641  gsumge0cl  46729  meadjiunlem  46823  hspmbllem2  46985  nthrucw  47244