Theorem nelsn 4630

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ≠ wne 2925  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-sn 4590

This theorem is referenced by:  frd  5595  fvn0fvelrn  6889  fvunsn  7153  fzdif1  13566  nnoddn2prmb  16784  lbsextlem4  21071  cnfldfun  21278  cnfldfunOLD  21291  obslbs  21639  logbgcd1irr  26704  upgrres1  29240  cycpmco2  33090  elrgspnlem4  33196  lindssn  33349  drngidlhash  33405  drnglidl1ne0  33446  drng0mxidl  33447  rsprprmprmidlb  33494  rprmirredb  33503  1arithufdlem4  33518  ig1pmindeg  33567  irngnminplynz  33702  algextdeglem4  33710  submateqlem1  33797  submateqlem2  33798  qqhval2  33972  derangsn  35157  ricdrng1  42516  prjspersym  42595  prjspreln0  42597  prjspnvs  42608  pr2eldif1  43543  pr2eldif2  43544  clsk3nimkb  44029  clsk1indlem1  44034  disjf1o  45185  cnrefiisplem  45827  fperdvper  45917  dvnmul  45941  wallispi  46068  etransc  46281  gsumge0cl  46369  meadjiunlem  46463  hspmbllem2  46625