This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-unc

Description: Define the uncurrying of F , which takes a function producing functions, and transforms it into a two-argument function. (Contributed by Mario Carneiro, 7-Jan-2017)

		Ref	Expression
	Assertion	df-unc	⊢ uncurry 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	⊢ 𝐹
1	0	cunc	⊢ uncurry 𝐹
2		vx	⊢ 𝑥
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5	3	cv	⊢ 𝑦
6	2	cv	⊢ 𝑥
7	6 0	cfv	⊢ ( 𝐹 ‘ 𝑥 )
8	4	cv	⊢ 𝑧
9	5 8 7	wbr	⊢ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧
10	9 2 3 4	coprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 }
11	1 10	wceq	⊢ uncurry 𝐹 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐹 ‘ 𝑥 ) 𝑧 }