Theorem nelsn 4630

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ≠ wne 2957  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-sn 4588

This theorem is used by:  frd  5616  fvn0fvelrn  6911  fvunsn  7181  fzdif1  13664  nnoddn2prmb  16911  chnccat  18720  drnglidl1ne0  20685  isdrng3lem2  20921  lbsextlem4  21354  cnfldfun  21605  obslbs  21949  logbgcd1irr  27039  upgrres1  29781  cycpmco2  33581  elrgspnlem4  33693  lindssn  33819  drngidlhash  33869  drng0mxidl  33886  rsprprmprmidlb  33941  rprmirredb  33950  1arithufdlem4  33965  ig1pmindeg  34020  irngnminplynz  34230  algextdeglem4  34238  submateqlem1  34325  submateqlem2  34326  qqhval2  34500  derangsn  35757  ricdrng1  43418  prjspersym  43461  prjspreln0  43463  prjspnvs  43474  pr2eldif1  44402  pr2eldif2  44403  clsk3nimkb  44888  clsk1indlem1  44893  disjf1o  46031  cnrefiisplem  46665  fperdvper  46755  dvnmul  46779  wallispi  46906  etransc  47119  gsumge0cl  47207  meadjiunlem  47301  hspmbllem2  47463  numtowerdt  47742