Theorem nelsn 4634

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146   ≠ wne 2960  {csn 4591

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-sn 4592

This theorem is used by:  frd  5620  fvn0fvelrn  6914  fvunsn  7181  fzdif1  13646  nnoddn2prmb  16891  chnccat  18700  drnglidl1ne0  20646  isdrng3lem2  20882  lbsextlem4  21315  cnfldfun  21566  obslbs  21910  logbgcd1irr  26990  upgrres1  29697  cycpmco2  33493  elrgspnlem4  33605  lindssn  33731  drngidlhash  33781  drng0mxidl  33798  rsprprmprmidlb  33853  rprmirredb  33862  1arithufdlem4  33877  ig1pmindeg  33932  irngnminplynz  34142  algextdeglem4  34150  submateqlem1  34237  submateqlem2  34238  qqhval2  34412  derangsn  35675  ricdrng1  43329  prjspersym  43372  prjspreln0  43374  prjspnvs  43385  pr2eldif1  44313  pr2eldif2  44314  clsk3nimkb  44799  clsk1indlem1  44804  disjf1o  45942  cnrefiisplem  46576  fperdvper  46666  dvnmul  46690  wallispi  46817  etransc  47030  gsumge0cl  47118  meadjiunlem  47212  hspmbllem2  47374  nthrucw  47640