Theorem nelsn 4622

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2141   ≠ wne 2956  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-sn 4580

This theorem is referenced by:  frd  5600  fvn0fvelrn  6891  fvunsn  7158  fzdif1  13604  nnoddn2prmb  16840  chnccat  18649  lbsextlem4  21219  cnfldfun  21426  obslbs  21770  logbgcd1irr  26847  upgrres1  29471  cycpmco2  33274  elrgspnlem4  33387  lindssn  33525  drngidlhash  33581  drnglidl1ne0  33624  drng0mxidl  33625  rsprprmprmidlb  33680  rprmirredb  33689  1arithufdlem4  33704  ig1pmindeg  33759  irngnminplynz  33970  algextdeglem4  33978  submateqlem1  34065  submateqlem2  34066  qqhval2  34240  derangsn  35481  ricdrng1  43107  prjspersym  43150  prjspreln0  43152  prjspnvs  43163  pr2eldif1  44091  pr2eldif2  44092  clsk3nimkb  44577  clsk1indlem1  44582  disjf1o  45730  cnrefiisplem  46364  fperdvper  46454  dvnmul  46478  wallispi  46605  etransc  46818  gsumge0cl  46906  meadjiunlem  47000  hspmbllem2  47162  nthrucw  47423