Theorem nelsn 4614

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

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

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 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-sn 4575

This theorem is referenced by:  frd  5580  fvn0fvelrn  6857  fvunsn  7108  nnoddn2prmb  16612  lbsextlem4  20530  cnfldfun  20716  obslbs  21044  logbgcd1irr  26051  upgrres1  27970  cycpmco2  31687  lindssn  31870  submateqlem1  32055  submateqlem2  32056  qqhval2  32230  derangsn  33431  prjspersym  40757  prjspreln0  40759  prjspvs  40760  prjspnvs  40770  pr2eldif1  41535  pr2eldif2  41536  clsk3nimkb  42023  clsk1indlem1  42028  disjf1o  43108  cnrefiisplem  43758  fperdvper  43848  dvnmul  43872  wallispi  43999  etransc  44212  gsumge0cl  44298  meadjiunlem  44392  hspmbllem2  44554