Theorem nelsn 4633

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ≠ wne 2926  {csn 4592

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-sn 4593

This theorem is referenced by:  frd  5598  fvn0fvelrn  6892  fvunsn  7156  fzdif1  13573  nnoddn2prmb  16791  lbsextlem4  21078  cnfldfun  21285  cnfldfunOLD  21298  obslbs  21646  logbgcd1irr  26711  upgrres1  29247  cycpmco2  33097  elrgspnlem4  33203  lindssn  33356  drngidlhash  33412  drnglidl1ne0  33453  drng0mxidl  33454  rsprprmprmidlb  33501  rprmirredb  33510  1arithufdlem4  33525  ig1pmindeg  33574  irngnminplynz  33709  algextdeglem4  33717  submateqlem1  33804  submateqlem2  33805  qqhval2  33979  derangsn  35164  ricdrng1  42523  prjspersym  42602  prjspreln0  42604  prjspnvs  42615  pr2eldif1  43550  pr2eldif2  43551  clsk3nimkb  44036  clsk1indlem1  44041  disjf1o  45192  cnrefiisplem  45834  fperdvper  45924  dvnmul  45948  wallispi  46075  etransc  46288  gsumge0cl  46376  meadjiunlem  46470  hspmbllem2  46632