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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-sn 4581

This theorem is referenced by:  frd  5581  fvn0fvelrn  6863  fvunsn  7125  fzdif1  13521  nnoddn2prmb  16741  chnccat  18549  lbsextlem4  21116  cnfldfun  21323  cnfldfunOLD  21336  obslbs  21685  logbgcd1irr  26760  upgrres1  29386  cycpmco2  33215  elrgspnlem4  33327  lindssn  33459  drngidlhash  33515  drnglidl1ne0  33556  drng0mxidl  33557  rsprprmprmidlb  33604  rprmirredb  33613  1arithufdlem4  33628  ig1pmindeg  33683  irngnminplynz  33869  algextdeglem4  33877  submateqlem1  33964  submateqlem2  33965  qqhval2  34139  derangsn  35364  ricdrng1  42783  prjspersym  42850  prjspreln0  42852  prjspnvs  42863  pr2eldif1  43795  pr2eldif2  43796  clsk3nimkb  44281  clsk1indlem1  44286  disjf1o  45435  cnrefiisplem  46073  fperdvper  46163  dvnmul  46187  wallispi  46314  etransc  46527  gsumge0cl  46615  meadjiunlem  46709  hspmbllem2  46871  nthrucw  47130