MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nelsn Structured version   Visualization version   GIF version

Theorem nelsn 4631
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
StepHypRef Expression
1 elsni 4608 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
21necon3ai 2969 1 (𝐴𝐵 → ¬ 𝐴 ∈ {𝐵})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  wne 2944  {csn 4591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-sn 4592
This theorem is referenced by:  frd  5597  fvn0fvelrn  6878  fvunsn  7130  nnoddn2prmb  16692  lbsextlem4  20638  cnfldfun  20824  obslbs  21152  logbgcd1irr  26160  upgrres1  28303  cycpmco2  32024  lindssn  32206  submateqlem1  32428  submateqlem2  32429  qqhval2  32603  derangsn  33804  ricdrng1  40746  prjspersym  40974  prjspreln0  40976  prjspvs  40977  prjspnvs  40987  pr2eldif1  41900  pr2eldif2  41901  clsk3nimkb  42386  clsk1indlem1  42391  disjf1o  43484  cnrefiisplem  44144  fperdvper  44234  dvnmul  44258  wallispi  44385  etransc  44598  gsumge0cl  44686  meadjiunlem  44780  hspmbllem2  44942
  Copyright terms: Public domain W3C validator