Theorem nelsn 4620

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

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

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 4580

This theorem is referenced by:  frd  5580  fvn0fvelrn  6855  fvunsn  7119  fzdif1  13527  nnoddn2prmb  16744  lbsextlem4  21087  cnfldfun  21294  cnfldfunOLD  21307  obslbs  21656  logbgcd1irr  26721  upgrres1  29277  cycpmco2  33094  elrgspnlem4  33204  lindssn  33334  drngidlhash  33390  drnglidl1ne0  33431  drng0mxidl  33432  rsprprmprmidlb  33479  rprmirredb  33488  1arithufdlem4  33503  ig1pmindeg  33553  irngnminplynz  33698  algextdeglem4  33706  submateqlem1  33793  submateqlem2  33794  qqhval2  33968  derangsn  35162  ricdrng1  42521  prjspersym  42600  prjspreln0  42602  prjspnvs  42613  pr2eldif1  43547  pr2eldif2  43548  clsk3nimkb  44033  clsk1indlem1  44038  disjf1o  45189  cnrefiisplem  45830  fperdvper  45920  dvnmul  45944  wallispi  46071  etransc  46284  gsumge0cl  46372  meadjiunlem  46466  hspmbllem2  46628