Definition df-propvar

Description: Variables in sentences of propositional calculus are encoded by appending a zero after the number of the variable. (Contributed by Thomas van Maaren, 21-Aug-2026)

	Ref	Expression
Assertion	df-propvar	Could not format assertion : No typesetting found for |- propvar = ( n e. NN |-> ( <" n "> ++ <" 0 "> ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpropvar	Could not format propvar : No typesetting found for class propvar with typecode class
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3	1	cv	$$setvarn$$
4	3	cs1	$$class⟨“n”⟩$$
5		cconcat	$$class\mathrm{++}$$
6		cc0	$$class0$$
7	6	cs1	$$class⟨“0”⟩$$
8	4 7 5	co	$$class\left(⟨“n”⟩\mathrm{++}⟨“0”⟩\right)$$
9	1 2 8	cmpt	$$class\left(n\in \mathbb{N}⟼⟨“n”⟩\mathrm{++}⟨“0”⟩\right)$$
10	0 9	wceq	Could not format propvar = ( n e. NN |-> ( <" n "> ++ <" 0 "> ) ) : No typesetting found for wff propvar = ( n e. NN |-> ( <" n "> ++ <" 0 "> ) ) with typecode wff