Theorem nelsn 4623

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144   ≠ wne 2955  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-sn 4585

This theorem is used by:  frd  5607  fvn0fvelrn  6917  fvunsn  7186  fzdif1  13744  nnoddn2prmb  16998  chnccat  18807  drnglidl1ne0  20776  isdrng3lem2  21013  lbsextlem4  21446  cnfldfun  21699  obslbs  22043  logbgcd1irr  27129  upgrres1  29901  cycpmco2  33742  elrgspnlem4  33854  lindssn  33981  drngidlhash  34031  drng0mxidl  34048  rsprprmprmidlb  34103  rprmirredb  34112  1arithufdlem4  34127  ig1pmindeg  34182  irngnminplynz  34392  algextdeglem4  34400  submateqlem1  34487  submateqlem2  34488  qqhval2  34662  derangsn  36023  ricdrng1  43699  prjspersym  43742  prjspreln0  43744  prjspnvs  43755  pr2eldif1  44662  pr2eldif2  44663  clsk3nimkb  45147  clsk1indlem1  45152  disjf1o  46313  cnrefiisplem  46946  fperdvper  47036  dvnmul  47060  wallispi  47187  etransc  47400  gsumge0cl  47488  meadjiunlem  47582  hspmbllem2  47744  numtowerdt  48023