Theorem nelsn 4627

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-sn 4585

This theorem is used by:  frd  5612  fvn0fvelrn  6907  fvunsn  7177  fzdif1  13660  nnoddn2prmb  16905  chnccat  18714  drnglidl1ne0  20679  isdrng3lem2  20915  lbsextlem4  21348  cnfldfun  21599  obslbs  21943  logbgcd1irr  27031  upgrres1  29773  cycpmco2  33573  elrgspnlem4  33685  lindssn  33811  drngidlhash  33861  drng0mxidl  33878  rsprprmprmidlb  33933  rprmirredb  33942  1arithufdlem4  33957  ig1pmindeg  34012  irngnminplynz  34222  algextdeglem4  34230  submateqlem1  34317  submateqlem2  34318  qqhval2  34492  derangsn  35749  ricdrng1  43410  prjspersym  43453  prjspreln0  43455  prjspnvs  43466  pr2eldif1  44394  pr2eldif2  44395  clsk3nimkb  44880  clsk1indlem1  44885  disjf1o  46023  cnrefiisplem  46657  fperdvper  46747  dvnmul  46771  wallispi  46898  etransc  47111  gsumge0cl  47199  meadjiunlem  47293  hspmbllem2  47455  numtowerdt  47734