Theorem nelsn 4664

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2099   ≠ wne 2930  {csn 4624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-sn 4625

This theorem is referenced by:  frd  5632  fvn0fvelrn  6922  fvunsn  7183  nnoddn2prmb  16808  lbsextlem4  21136  cnfldfun  21351  cnfldfunOLD  21364  obslbs  21722  logbgcd1irr  26817  upgrres1  29244  cycpmco2  33013  lindssn  33257  drngidlhash  33313  drnglidl1ne0  33354  drng0mxidl  33355  rsprprmprmidlb  33402  rprmirredb  33411  1arithufdlem4  33426  ig1pmindeg  33473  irngnminplynz  33585  algextdeglem4  33591  submateqlem1  33633  submateqlem2  33634  qqhval2  33808  derangsn  35009  ricdrng1  42216  prjspersym  42295  prjspreln0  42297  prjspnvs  42308  pr2eldif1  43256  pr2eldif2  43257  clsk3nimkb  43742  clsk1indlem1  43747  disjf1o  44832  cnrefiisplem  45484  fperdvper  45574  dvnmul  45598  wallispi  45725  etransc  45938  gsumge0cl  46026  meadjiunlem  46120  hspmbllem2  46282