Theorem nelsn 4352

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-v 3353  df-sn 4318

This theorem is referenced by:  fvunsn  6590  nnoddn2prmb  15726  lbsextlem4  19377  cnfldfunALT  19975  obslbs  20292  upgrres1  26429  submateqlem1  30214  submateqlem2  30215  qqhval2  30367  derangsn  31491  clsk3nimkb  38865  clsk1indlem1  38870  disjf1o  39899  cnrefiisplem  40574  fperdvper  40652  dvnmul  40677  wallispi  40805  etransc  41018  gsumge0cl  41106  meadjiunlem  41200  hspmbllem2  41362