Theorem nelsn 4634

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149   ≠ wne 2964  {csn 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-sn 4592

This theorem is referenced by:  frd  5616  fvn0fvelrn  6908  fvunsn  7175  fzdif1  13629  nnoddn2prmb  16869  chnccat  18678  drnglidl1ne0  20598  lbsextlem4  21259  cnfldfun  21501  obslbs  21845  logbgcd1irr  26921  upgrres1  29600  cycpmco2  33390  elrgspnlem4  33502  lindssn  33631  drngidlhash  33682  drng0mxidl  33699  rsprprmprmidlb  33754  rprmirredb  33763  1arithufdlem4  33778  ig1pmindeg  33833  irngnminplynz  34043  algextdeglem4  34051  submateqlem1  34138  submateqlem2  34139  qqhval2  34313  derangsn  35557  ricdrng1  43183  prjspersym  43226  prjspreln0  43228  prjspnvs  43239  pr2eldif1  44167  pr2eldif2  44168  clsk3nimkb  44653  clsk1indlem1  44658  disjf1o  45796  cnrefiisplem  46430  fperdvper  46520  dvnmul  46544  wallispi  46671  etransc  46884  gsumge0cl  46972  meadjiunlem  47066  hspmbllem2  47228  nthrucw  47489