Definition df-propneg 38551

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.)

Assertion

Ref	Expression
df-propneg	⊢ prop¬ = (𝑥 ∈ V ↦ (𝑥 ++ ⟨“1”⟩))

Detailed syntax breakdown of Definition df-propneg

Step	Hyp	Ref	Expression
1		cpropneg 38548	. 2 class prop¬
2		vx	. . 3 setvar 𝑥
3		cvv 3450	. . 3 class V
4	2	cv 1569	. . . 4 class 𝑥
5		c1 11158	. . . . 5 class 1
6	5	cs1 14695	. . . 4 class ⟨“1”⟩
7		cconcat 14668	. . . 4 class ++
8	4, 6, 7	co 7409	. . 3 class (𝑥 ++ ⟨“1”⟩)
9	2, 3, 8	cmpt 5186	. 2 class (𝑥 ∈ V ↦ (𝑥 ++ ⟨“1”⟩))
10	1, 9	wceq 1570	1 wff prop¬ = (𝑥 ∈ V ↦ (𝑥 ++ ⟨“1”⟩))

This definition is used by: (None)