Definition df-propneg

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¬ = ( 𝑥 ∈ V ↦ ( 𝑥 ++ ⟨“ 1 ”⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpropneg	⊢ prop¬
1		vx	⊢ 𝑥
2		cvv	⊢ V
3	1	cv	⊢ 𝑥
4		cconcat	⊢ ++
5		c1	⊢ 1
6	5	cs1	⊢ ⟨“ 1 ”⟩
7	3 6 4	co	⊢ ( 𝑥 ++ ⟨“ 1 ”⟩ )
8	1 2 7	cmpt	⊢ ( 𝑥 ∈ V ↦ ( 𝑥 ++ ⟨“ 1 ”⟩ ) )
9	0 8	wceq	⊢ prop¬ = ( 𝑥 ∈ V ↦ ( 𝑥 ++ ⟨“ 1 ”⟩ ) )