![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nelsn | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
nelsn | ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsni 4489 | . 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | |
2 | 1 | necon3ai 3009 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2081 ≠ wne 2984 {csn 4472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-sn 4473 |
This theorem is referenced by: fvunsn 6804 nnoddn2prmb 15979 lbsextlem4 19623 cnfldfunALT 20240 obslbs 20556 logbgcd1irr 25053 upgrres1 26778 lindssn 30585 submateqlem1 30687 submateqlem2 30688 qqhval2 30840 derangsn 32025 prjspersym 38754 prjspreln0 38756 prjspvs 38757 pr2eldif1 39398 pr2eldif2 39399 clsk3nimkb 39875 clsk1indlem1 39880 disjf1o 40992 cnrefiisplem 41652 fperdvper 41744 dvnmul 41769 wallispi 41897 etransc 42110 gsumge0cl 42195 meadjiunlem 42289 hspmbllem2 42451 |
Copyright terms: Public domain | W3C validator |