Theorem nelsn 4601

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   ≠ wne 2943  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-sn 4562

This theorem is referenced by:  frd  5548  fvunsn  7051  nnoddn2prmb  16514  lbsextlem4  20423  cnfldfun  20609  obslbs  20937  logbgcd1irr  25944  upgrres1  27680  cycpmco2  31400  lindssn  31573  submateqlem1  31757  submateqlem2  31758  qqhval2  31932  derangsn  33132  prjspersym  40446  prjspreln0  40448  prjspvs  40449  prjspnvs  40459  pr2eldif1  41161  pr2eldif2  41162  clsk3nimkb  41650  clsk1indlem1  41655  disjf1o  42729  cnrefiisplem  43370  fperdvper  43460  dvnmul  43484  wallispi  43611  etransc  43824  gsumge0cl  43909  meadjiunlem  44003  hspmbllem2  44165