Theorem nelsn 4611

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ≠ wne 2933  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-sn 4569

This theorem is referenced by:  frd  5581  fvn0fvelrn  6863  fvunsn  7127  fzdif1  13550  nnoddn2prmb  16775  chnccat  18583  lbsextlem4  21151  cnfldfun  21358  cnfldfunOLD  21371  obslbs  21720  logbgcd1irr  26771  upgrres1  29396  cycpmco2  33209  elrgspnlem4  33321  lindssn  33453  drngidlhash  33509  drnglidl1ne0  33550  drng0mxidl  33551  rsprprmprmidlb  33598  rprmirredb  33607  1arithufdlem4  33622  ig1pmindeg  33677  irngnminplynz  33872  algextdeglem4  33880  submateqlem1  33967  submateqlem2  33968  qqhval2  34142  derangsn  35368  ricdrng1  42987  prjspersym  43054  prjspreln0  43056  prjspnvs  43067  pr2eldif1  43999  pr2eldif2  44000  clsk3nimkb  44485  clsk1indlem1  44490  disjf1o  45639  cnrefiisplem  46275  fperdvper  46365  dvnmul  46389  wallispi  46516  etransc  46729  gsumge0cl  46817  meadjiunlem  46911  hspmbllem2  47073  nthrucw  47332