Theorem nelsn 4620

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ≠ wne 2930  {csn 4577

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-sn 4578

This theorem is referenced by:  frd  5578  fvn0fvelrn  6860  fvunsn  7122  fzdif1  13515  nnoddn2prmb  16735  chnccat  18542  lbsextlem4  21108  cnfldfun  21315  cnfldfunOLD  21328  obslbs  21677  logbgcd1irr  26741  upgrres1  29302  cycpmco2  33113  elrgspnlem4  33223  lindssn  33354  drngidlhash  33410  drnglidl1ne0  33451  drng0mxidl  33452  rsprprmprmidlb  33499  rprmirredb  33508  1arithufdlem4  33523  ig1pmindeg  33573  irngnminplynz  33736  algextdeglem4  33744  submateqlem1  33831  submateqlem2  33832  qqhval2  34006  derangsn  35225  ricdrng1  42636  prjspersym  42715  prjspreln0  42717  prjspnvs  42728  pr2eldif1  43661  pr2eldif2  43662  clsk3nimkb  44147  clsk1indlem1  44152  disjf1o  45302  cnrefiisplem  45941  fperdvper  46031  dvnmul  46055  wallispi  46182  etransc  46395  gsumge0cl  46483  meadjiunlem  46577  hspmbllem2  46739  nthrucw  46998