Definition df-propimp

Description: The implication between two sentences of propositional calculus is encoded by concatenating the two sentences and appending a two at the end. (Contributed by Thomas van Maaren, 21-Aug-2026)

	Ref	Expression
Assertion	df-propimp	⊢ prop→ = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( ( 𝑥 ++ 𝑦 ) ++ ⟨“ 2 ”⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpropimp	⊢ prop→
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		cconcat	⊢ ++
6	3	cv	⊢ 𝑦
7	4 6 5	co	⊢ ( 𝑥 ++ 𝑦 )
8		c2	⊢ 2
9	8	cs1	⊢ ⟨“ 2 ”⟩
10	7 9 5	co	⊢ ( ( 𝑥 ++ 𝑦 ) ++ ⟨“ 2 ”⟩ )
11	1 3 2 2 10	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( ( 𝑥 ++ 𝑦 ) ++ ⟨“ 2 ”⟩ ) )
12	0 11	wceq	⊢ prop→ = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( ( 𝑥 ++ 𝑦 ) ++ ⟨“ 2 ”⟩ ) )