Theorem nelsn 4668

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105   ≠ wne 2939  {csn 4628

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-sn 4629

This theorem is referenced by:  frd  5635  fvn0fvelrn  6922  fvunsn  7179  nnoddn2prmb  16753  lbsextlem4  21007  cnfldfun  21244  obslbs  21594  logbgcd1irr  26639  upgrres1  29002  cycpmco2  32727  lindssn  32933  drngidlhash  32991  drnglidl1ne0  33030  drng0mxidl  33031  ig1pmindeg  33112  irngnminplynz  33225  algextdeglem4  33230  submateqlem1  33250  submateqlem2  33251  qqhval2  33425  derangsn  34624  gg-cnfldfun  35643  ricdrng1  41566  prjspersym  41811  prjspreln0  41813  prjspvs  41814  prjspnvs  41824  pr2eldif1  42767  pr2eldif2  42768  clsk3nimkb  43253  clsk1indlem1  43258  disjf1o  44348  cnrefiisplem  45003  fperdvper  45093  dvnmul  45117  wallispi  45244  etransc  45457  gsumge0cl  45545  meadjiunlem  45639  hspmbllem2  45801