Definition df-propvar 38550

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

Assertion

Ref	Expression
df-propvar	⊢ propvar = (𝑛 ∈ ℕ ↦ (⟨“𝑛”⟩ ++ ⟨“0”⟩))

Detailed syntax breakdown of Definition df-propvar

Step	Hyp	Ref	Expression
1		cpropvar 38547	. 2 class propvar
2		vn	. . 3 setvar 𝑛
3		cn 12290	. . 3 class ℕ
4	2	cv 1569	. . . . 5 class 𝑛
5	4	cs1 14695	. . . 4 class ⟨“𝑛”⟩
6		cc0 11157	. . . . 5 class 0
7	6	cs1 14695	. . . 4 class ⟨“0”⟩
8		cconcat 14668	. . . 4 class ++
9	5, 7, 8	co 7409	. . 3 class (⟨“𝑛”⟩ ++ ⟨“0”⟩)
10	2, 3, 9	cmpt 5186	. 2 class (𝑛 ∈ ℕ ↦ (⟨“𝑛”⟩ ++ ⟨“0”⟩))
11	1, 10	wceq 1570	1 wff propvar = (𝑛 ∈ ℕ ↦ (⟨“𝑛”⟩ ++ ⟨“0”⟩))

This definition is used by: (None)