Theorem nelsn 4631

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-sn 4592

This theorem is referenced by:  frd  5597  fvn0fvelrn  6878  fvunsn  7130  nnoddn2prmb  16696  lbsextlem4  20681  cnfldfun  20845  obslbs  21173  logbgcd1irr  26181  upgrres1  28324  cycpmco2  32052  lindssn  32238  submateqlem1  32477  submateqlem2  32478  qqhval2  32652  derangsn  33851  ricdrng1  40778  prjspersym  41003  prjspreln0  41005  prjspvs  41006  prjspnvs  41016  pr2eldif1  41948  pr2eldif2  41949  clsk3nimkb  42434  clsk1indlem1  42439  disjf1o  43532  cnrefiisplem  44190  fperdvper  44280  dvnmul  44304  wallispi  44431  etransc  44644  gsumge0cl  44732  meadjiunlem  44826  hspmbllem2  44988