Theorem nelsn 4581

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110   ≠ wne 2940  {csn 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-sn 4542

This theorem is referenced by:  fvunsn  6994  nnoddn2prmb  16366  lbsextlem4  20198  cnfldfunALT  20376  obslbs  20692  logbgcd1irr  25677  upgrres1  27401  cycpmco2  31119  lindssn  31287  submateqlem1  31471  submateqlem2  31472  qqhval2  31644  derangsn  32845  prjspersym  40154  prjspreln0  40156  prjspvs  40157  prjspnvs  40167  pr2eldif1  40837  pr2eldif2  40838  clsk3nimkb  41327  clsk1indlem1  41332  disjf1o  42402  cnrefiisplem  43045  fperdvper  43135  dvnmul  43159  wallispi  43286  etransc  43499  gsumge0cl  43584  meadjiunlem  43678  hspmbllem2  43840