Theorem nelsn 4598

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119   ≠ wne 2934  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-sn 4556

This theorem is referenced by:  frd  5575  fvn0fvelrn  6856  fvunsn  7123  fzdif1  13550  nnoddn2prmb  16775  chnccat  18583  lbsextlem4  21154  cnfldfun  21361  obslbs  21705  logbgcd1irr  26776  upgrres1  29400  cycpmco2  33214  elrgspnlem4  33326  lindssn  33461  drngidlhash  33517  drnglidl1ne0  33558  drng0mxidl  33559  rsprprmprmidlb  33606  rprmirredb  33615  1arithufdlem4  33630  ig1pmindeg  33685  irngnminplynz  33896  algextdeglem4  33904  submateqlem1  33991  submateqlem2  33992  qqhval2  34166  derangsn  35398  ricdrng1  43014  prjspersym  43057  prjspreln0  43059  prjspnvs  43070  pr2eldif1  43998  pr2eldif2  43999  clsk3nimkb  44484  clsk1indlem1  44489  disjf1o  45638  cnrefiisplem  46272  fperdvper  46362  dvnmul  46386  wallispi  46513  etransc  46726  gsumge0cl  46814  meadjiunlem  46908  hspmbllem2  47070  nthrucw  47331