Theorem nelsn 4510

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2081   ≠ wne 2984  {csn 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-sn 4473

This theorem is referenced by:  fvunsn  6804  nnoddn2prmb  15979  lbsextlem4  19623  cnfldfunALT  20240  obslbs  20556  logbgcd1irr  25053  upgrres1  26778  lindssn  30585  submateqlem1  30687  submateqlem2  30688  qqhval2  30840  derangsn  32025  prjspersym  38754  prjspreln0  38756  prjspvs  38757  pr2eldif1  39398  pr2eldif2  39399  clsk3nimkb  39875  clsk1indlem1  39880  disjf1o  40992  cnrefiisplem  41652  fperdvper  41744  dvnmul  41769  wallispi  41897  etransc  42110  gsumge0cl  42195  meadjiunlem  42289  hspmbllem2  42451