Theorem nelsn 4598

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

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

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-ne 3016  df-sn 4561

This theorem is referenced by:  fvunsn  6934  nnoddn2prmb  16145  lbsextlem4  19928  cnfldfunALT  20553  obslbs  20869  logbgcd1irr  25370  upgrres1  27093  cycpmco2  30796  lindssn  30961  submateqlem1  31096  submateqlem2  31097  qqhval2  31244  derangsn  32438  prjspersym  39333  prjspreln0  39335  prjspvs  39336  pr2eldif1  39987  pr2eldif2  39988  clsk3nimkb  40464  clsk1indlem1  40469  disjf1o  41526  cnrefiisplem  42184  fperdvper  42277  dvnmul  42302  wallispi  42429  etransc  42642  gsumge0cl  42727  meadjiunlem  42821  hspmbllem2  42983