Theorem nelsn 4670

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105   ≠ wne 2937  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-sn 4631

This theorem is referenced by:  frd  5644  fvn0fvelrn  6937  fvunsn  7198  fzdif1  13641  nnoddn2prmb  16846  lbsextlem4  21180  cnfldfun  21395  cnfldfunOLD  21408  obslbs  21767  logbgcd1irr  26851  upgrres1  29344  cycpmco2  33135  elrgspnlem4  33234  lindssn  33385  drngidlhash  33441  drnglidl1ne0  33482  drng0mxidl  33483  rsprprmprmidlb  33530  rprmirredb  33539  1arithufdlem4  33554  ig1pmindeg  33601  irngnminplynz  33719  algextdeglem4  33725  submateqlem1  33767  submateqlem2  33768  qqhval2  33944  derangsn  35154  ricdrng1  42514  prjspersym  42593  prjspreln0  42595  prjspnvs  42606  pr2eldif1  43543  pr2eldif2  43544  clsk3nimkb  44029  clsk1indlem1  44034  disjf1o  45133  cnrefiisplem  45784  fperdvper  45874  dvnmul  45898  wallispi  46025  etransc  46238  gsumge0cl  46326  meadjiunlem  46420  hspmbllem2  46582