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	⊢ propvar = ( 𝑛 ∈ ℕ ↦ ( ⟨“ 𝑛 ”⟩ ++ ⟨“ 0 ”⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpropvar	⊢ propvar
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3	1	cv	⊢ 𝑛
4	3	cs1	⊢ ⟨“ 𝑛 ”⟩
5		cconcat	⊢ ++
6		cc0	⊢ 0
7	6	cs1	⊢ ⟨“ 0 ”⟩
8	4 7 5	co	⊢ ( ⟨“ 𝑛 ”⟩ ++ ⟨“ 0 ”⟩ )
9	1 2 8	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( ⟨“ 𝑛 ”⟩ ++ ⟨“ 0 ”⟩ ) )
10	0 9	wceq	⊢ propvar = ( 𝑛 ∈ ℕ ↦ ( ⟨“ 𝑛 ”⟩ ++ ⟨“ 0 ”⟩ ) )