Theorem nelsn 4626

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ≠ wne 2925  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-sn 4586

This theorem is referenced by:  frd  5588  fvn0fvelrn  6871  fvunsn  7135  fzdif1  13542  nnoddn2prmb  16760  lbsextlem4  21047  cnfldfun  21254  cnfldfunOLD  21267  obslbs  21615  logbgcd1irr  26680  upgrres1  29216  cycpmco2  33063  elrgspnlem4  33169  lindssn  33322  drngidlhash  33378  drnglidl1ne0  33419  drng0mxidl  33420  rsprprmprmidlb  33467  rprmirredb  33476  1arithufdlem4  33491  ig1pmindeg  33540  irngnminplynz  33675  algextdeglem4  33683  submateqlem1  33770  submateqlem2  33771  qqhval2  33945  derangsn  35130  ricdrng1  42489  prjspersym  42568  prjspreln0  42570  prjspnvs  42581  pr2eldif1  43516  pr2eldif2  43517  clsk3nimkb  44002  clsk1indlem1  44007  disjf1o  45158  cnrefiisplem  45800  fperdvper  45890  dvnmul  45914  wallispi  46041  etransc  46254  gsumge0cl  46342  meadjiunlem  46436  hspmbllem2  46598