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	Could not format assertion : No typesetting found for |- prop-. = ( x e. _V |-> ( x ++ <" 1 "> ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpropneg	Could not format prop-. : No typesetting found for class prop-. with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarx$$
4		cconcat	$$class\mathrm{++}$$
5		c1	$$class1$$
6	5	cs1	$$class⟨“1”⟩$$
7	3 6 4	co	$$class\left(x\mathrm{++}⟨“1”⟩\right)$$
8	1 2 7	cmpt	$$class\left(x\in \mathrm{V}⟼x\mathrm{++}⟨“1”⟩\right)$$
9	0 8	wceq	Could not format prop-. = ( x e. _V |-> ( x ++ <" 1 "> ) ) : No typesetting found for wff prop-. = ( x e. _V |-> ( x ++ <" 1 "> ) ) with typecode wff