| 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 4643 | . 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | |
| 2 | 1 | necon3ai 2965 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵}) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2108 ≠ wne 2940 {csn 4626 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-sn 4627 |
| This theorem is referenced by: frd 5641 fvn0fvelrn 6937 fvunsn 7199 fzdif1 13645 nnoddn2prmb 16851 lbsextlem4 21163 cnfldfun 21378 cnfldfunOLD 21391 obslbs 21750 logbgcd1irr 26837 upgrres1 29330 cycpmco2 33153 elrgspnlem4 33249 lindssn 33406 drngidlhash 33462 drnglidl1ne0 33503 drng0mxidl 33504 rsprprmprmidlb 33551 rprmirredb 33560 1arithufdlem4 33575 ig1pmindeg 33622 irngnminplynz 33755 algextdeglem4 33761 submateqlem1 33806 submateqlem2 33807 qqhval2 33983 derangsn 35175 ricdrng1 42538 prjspersym 42617 prjspreln0 42619 prjspnvs 42630 pr2eldif1 43567 pr2eldif2 43568 clsk3nimkb 44053 clsk1indlem1 44058 disjf1o 45196 cnrefiisplem 45844 fperdvper 45934 dvnmul 45958 wallispi 46085 etransc 46298 gsumge0cl 46386 meadjiunlem 46480 hspmbllem2 46642 |
| Copyright terms: Public domain | W3C validator |