Theorem nelsn 4688

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ≠ wne 2946  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-sn 4649

This theorem is referenced by:  frd  5656  fvn0fvelrn  6951  fvunsn  7213  nnoddn2prmb  16860  lbsextlem4  21186  cnfldfun  21401  cnfldfunOLD  21414  obslbs  21773  logbgcd1irr  26855  upgrres1  29348  cycpmco2  33126  lindssn  33371  drngidlhash  33427  drnglidl1ne0  33468  drng0mxidl  33469  rsprprmprmidlb  33516  rprmirredb  33525  1arithufdlem4  33540  ig1pmindeg  33587  irngnminplynz  33705  algextdeglem4  33711  submateqlem1  33753  submateqlem2  33754  qqhval2  33928  derangsn  35138  ricdrng1  42483  prjspersym  42562  prjspreln0  42564  prjspnvs  42575  pr2eldif1  43516  pr2eldif2  43517  clsk3nimkb  44002  clsk1indlem1  44007  disjf1o  45098  cnrefiisplem  45750  fperdvper  45840  dvnmul  45864  wallispi  45991  etransc  46204  gsumge0cl  46292  meadjiunlem  46386  hspmbllem2  46548