Description: The negation of a sentence of propositional calculus is encoded by appending a one after the sentence. (Contributed by Thomas van Maaren, 21-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-propneg | |- prop-. = ( x e. _V |-> ( x ++ <" 1 "> ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cpropneg | |- prop-. |
|
| 1 | vx | |- x |
|
| 2 | cvv | |- _V |
|
| 3 | 1 | cv | |- x |
| 4 | cconcat | |- ++ |
|
| 5 | c1 | |- 1 |
|
| 6 | 5 | cs1 | |- <" 1 "> |
| 7 | 3 6 4 | co | |- ( x ++ <" 1 "> ) |
| 8 | 1 2 7 | cmpt | |- ( x e. _V |-> ( x ++ <" 1 "> ) ) |
| 9 | 0 8 | wceq | |- prop-. = ( x e. _V |-> ( x ++ <" 1 "> ) ) |