Theorem nelsn 4598

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ≠ wne 2942  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-sn 4559

This theorem is referenced by:  frd  5539  fvunsn  7033  nnoddn2prmb  16442  lbsextlem4  20338  cnfldfunALT  20523  obslbs  20847  logbgcd1irr  25849  upgrres1  27583  cycpmco2  31302  lindssn  31475  submateqlem1  31659  submateqlem2  31660  qqhval2  31832  derangsn  33032  prjspersym  40367  prjspreln0  40369  prjspvs  40370  prjspnvs  40380  pr2eldif1  41050  pr2eldif2  41051  clsk3nimkb  41539  clsk1indlem1  41544  disjf1o  42618  cnrefiisplem  43260  fperdvper  43350  dvnmul  43374  wallispi  43501  etransc  43714  gsumge0cl  43799  meadjiunlem  43893  hspmbllem2  44055