Metamath Proof Explorer

Definition df-bj-unc

Description: Define uncurrying. See also df-unc . (Contributed by BJ, 11-Apr-2020)

Ref Expression
Assertion df-bj-unc ⊢ uncurry_ = x ∈ V , y ∈ V , z ∈ V ⟼ f ∈ x ⟶Set y ⟶Set z ⟼ a ∈ x , b ∈ y ⟼ f ⁡ a ⁡ b

Detailed syntax breakdown

Step Hyp Ref Expression
0 cunc- class uncurry_
1 vx setvar x
2 cvv class V
3 vy setvar y
4 vz setvar z
5 vf setvar f
6 1 cv setvar x
7 csethom class ⟶Set
8 3 cv setvar y
9 4 cv setvar z
10 8 9 7 co class y ⟶Set z
11 6 10 7 co class x ⟶Set y ⟶Set z
12 va setvar a
13 vb setvar b
14 5 cv setvar f
15 12 cv setvar a
16 15 14 cfv class f ⁡ a
17 13 cv setvar b
18 17 16 cfv class f ⁡ a ⁡ b
19 12 13 6 8 18 cmpo class a ∈ x , b ∈ y ⟼ f ⁡ a ⁡ b
20 5 11 19 cmpt class f ∈ x ⟶Set y ⟶Set z ⟼ a ∈ x , b ∈ y ⟼ f ⁡ a ⁡ b
21 1 3 4 2 2 2 20 cmpt3 class x ∈ V , y ∈ V , z ∈ V ⟼ f ∈ x ⟶Set y ⟶Set z ⟼ a ∈ x , b ∈ y ⟼ f ⁡ a ⁡ b
22 0 21 wceq wff uncurry_ = x ∈ V , y ∈ V , z ∈ V ⟼ f ∈ x ⟶Set y ⟶Set z ⟼ a ∈ x , b ∈ y ⟼ f ⁡ a ⁡ b