![]() |
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 4608 | . 2 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | |
2 | 1 | necon3ai 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 |