Theorem nelsn 4632

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143   ≠ wne 2958  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-sn 4590

This theorem is referenced by:  frd  5618  fvn0fvelrn  6910  fvunsn  7177  fzdif1  13629  nnoddn2prmb  16868  chnccat  18677  drnglidl1ne0  20616  isdrng3lem2  20852  lbsextlem4  21285  cnfldfun  21536  obslbs  21880  logbgcd1irr  26959  upgrres1  29663  cycpmco2  33453  elrgspnlem4  33565  lindssn  33691  drngidlhash  33741  drng0mxidl  33758  rsprprmprmidlb  33813  rprmirredb  33822  1arithufdlem4  33837  ig1pmindeg  33892  irngnminplynz  34102  algextdeglem4  34110  submateqlem1  34197  submateqlem2  34198  qqhval2  34372  derangsn  35662  ricdrng1  43296  prjspersym  43339  prjspreln0  43341  prjspnvs  43352  pr2eldif1  44280  pr2eldif2  44281  clsk3nimkb  44766  clsk1indlem1  44771  disjf1o  45909  cnrefiisplem  46543  fperdvper  46633  dvnmul  46657  wallispi  46784  etransc  46997  gsumge0cl  47085  meadjiunlem  47179  hspmbllem2  47341  nthrucw  47607