![]() |
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 4641 | . 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | |
2 | 1 | necon3ai 2955 | 1 ⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 ∈ {𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2099 ≠ wne 2930 {csn 4624 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-sn 4625 |
This theorem is referenced by: frd 5632 fvn0fvelrn 6922 fvunsn 7183 nnoddn2prmb 16808 lbsextlem4 21136 cnfldfun 21351 cnfldfunOLD 21364 obslbs 21722 logbgcd1irr 26817 upgrres1 29244 cycpmco2 33013 lindssn 33257 drngidlhash 33313 drnglidl1ne0 33354 drng0mxidl 33355 rsprprmprmidlb 33402 rprmirredb 33411 1arithufdlem4 33426 ig1pmindeg 33473 irngnminplynz 33585 algextdeglem4 33591 submateqlem1 33633 submateqlem2 33634 qqhval2 33808 derangsn 35009 ricdrng1 42216 prjspersym 42295 prjspreln0 42297 prjspnvs 42308 pr2eldif1 43256 pr2eldif2 43257 clsk3nimkb 43742 clsk1indlem1 43747 disjf1o 44832 cnrefiisplem 45484 fperdvper 45574 dvnmul 45598 wallispi 45725 etransc 45938 gsumge0cl 46026 meadjiunlem 46120 hspmbllem2 46282 |
Copyright terms: Public domain | W3C validator |