Theorem nelsn 4666

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ≠ wne 2940  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-sn 4627

This theorem is referenced by:  frd  5641  fvn0fvelrn  6937  fvunsn  7199  fzdif1  13645  nnoddn2prmb  16851  lbsextlem4  21163  cnfldfun  21378  cnfldfunOLD  21391  obslbs  21750  logbgcd1irr  26837  upgrres1  29330  cycpmco2  33153  elrgspnlem4  33249  lindssn  33406  drngidlhash  33462  drnglidl1ne0  33503  drng0mxidl  33504  rsprprmprmidlb  33551  rprmirredb  33560  1arithufdlem4  33575  ig1pmindeg  33622  irngnminplynz  33755  algextdeglem4  33761  submateqlem1  33806  submateqlem2  33807  qqhval2  33983  derangsn  35175  ricdrng1  42538  prjspersym  42617  prjspreln0  42619  prjspnvs  42630  pr2eldif1  43567  pr2eldif2  43568  clsk3nimkb  44053  clsk1indlem1  44058  disjf1o  45196  cnrefiisplem  45844  fperdvper  45934  dvnmul  45958  wallispi  46085  etransc  46298  gsumge0cl  46386  meadjiunlem  46480  hspmbllem2  46642