Theorem nelsn 4642

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-sn 4602

This theorem is referenced by:  frd  5610  fvn0fvelrn  6906  fvunsn  7170  fzdif1  13620  nnoddn2prmb  16831  lbsextlem4  21120  cnfldfun  21327  cnfldfunOLD  21340  obslbs  21688  logbgcd1irr  26754  upgrres1  29238  cycpmco2  33090  elrgspnlem4  33186  lindssn  33339  drngidlhash  33395  drnglidl1ne0  33436  drng0mxidl  33437  rsprprmprmidlb  33484  rprmirredb  33493  1arithufdlem4  33508  ig1pmindeg  33557  irngnminplynz  33692  algextdeglem4  33700  submateqlem1  33784  submateqlem2  33785  qqhval2  33959  derangsn  35138  ricdrng1  42498  prjspersym  42577  prjspreln0  42579  prjspnvs  42590  pr2eldif1  43525  pr2eldif2  43526  clsk3nimkb  44011  clsk1indlem1  44016  disjf1o  45163  cnrefiisplem  45806  fperdvper  45896  dvnmul  45920  wallispi  46047  etransc  46260  gsumge0cl  46348  meadjiunlem  46442  hspmbllem2  46604