Theorem nelsn 4605

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ≠ wne 3016  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-sn 4568

This theorem is referenced by:  fvunsn  6941  nnoddn2prmb  16150  lbsextlem4  19933  cnfldfunALT  20558  obslbs  20874  logbgcd1irr  25372  upgrres1  27095  cycpmco2  30775  lindssn  30939  submateqlem1  31072  submateqlem2  31073  qqhval2  31223  derangsn  32417  prjspersym  39277  prjspreln0  39279  prjspvs  39280  pr2eldif1  39933  pr2eldif2  39934  clsk3nimkb  40410  clsk1indlem1  40415  disjf1o  41472  cnrefiisplem  42130  fperdvper  42223  dvnmul  42248  wallispi  42375  etransc  42588  gsumge0cl  42673  meadjiunlem  42767  hspmbllem2  42929