Theorem nelsn 4610

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 2957	1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵})

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-sn 4568

This theorem is referenced by:  frd  5588  fvn0fvelrn  6869  fvunsn  7134  fzdif1  13559  nnoddn2prmb  16784  chnccat  18592  lbsextlem4  21159  cnfldfun  21366  obslbs  21710  logbgcd1irr  26758  upgrres1  29382  cycpmco2  33194  elrgspnlem4  33306  lindssn  33438  drngidlhash  33494  drnglidl1ne0  33535  drng0mxidl  33536  rsprprmprmidlb  33583  rprmirredb  33592  1arithufdlem4  33607  ig1pmindeg  33662  irngnminplynz  33856  algextdeglem4  33864  submateqlem1  33951  submateqlem2  33952  qqhval2  34126  derangsn  35352  ricdrng1  42973  prjspersym  43040  prjspreln0  43042  prjspnvs  43053  pr2eldif1  43981  pr2eldif2  43982  clsk3nimkb  44467  clsk1indlem1  44472  disjf1o  45621  cnrefiisplem  46257  fperdvper  46347  dvnmul  46371  wallispi  46498  etransc  46711  gsumge0cl  46799  meadjiunlem  46893  hspmbllem2  47055  nthrucw  47316