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

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
StepHypRef Expression
1 elsni 4334 . 2 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
21necon3ai 2968 1 (𝐴𝐵 → ¬ 𝐴 ∈ {𝐵})
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator