Theorem nelsn 4620

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-sn 4578

This theorem is referenced by:  frd  5578  fvn0fvelrn  6860  fvunsn  7122  fzdif1  13512  nnoddn2prmb  16732  chnccat  18540  lbsextlem4  21107  cnfldfun  21314  cnfldfunOLD  21327  obslbs  21676  logbgcd1irr  26751  upgrres1  29312  cycpmco2  33143  elrgspnlem4  33255  lindssn  33387  drngidlhash  33443  drnglidl1ne0  33484  drng0mxidl  33485  rsprprmprmidlb  33532  rprmirredb  33541  1arithufdlem4  33556  ig1pmindeg  33611  irngnminplynz  33797  algextdeglem4  33805  submateqlem1  33892  submateqlem2  33893  qqhval2  34067  derangsn  35286  ricdrng1  42698  prjspersym  42765  prjspreln0  42767  prjspnvs  42778  pr2eldif1  43711  pr2eldif2  43712  clsk3nimkb  44197  clsk1indlem1  44202  disjf1o  45351  cnrefiisplem  45989  fperdvper  46079  dvnmul  46103  wallispi  46230  etransc  46443  gsumge0cl  46531  meadjiunlem  46625  hspmbllem2  46787  nthrucw  47046