Metamath Proof Explorer

Definition df-bj-cur

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccur- class curry_
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 3 cv setvar y
8 6 7 cxp class x × y
9 csethom class ⟶Set
10 4 cv setvar z
11 8 10 9 co class x × y ⟶Set z
12 va setvar a
13 vb setvar b
14 5 cv setvar f
15 12 cv setvar a
16 13 cv setvar b
17 15 16 cop class a b
18 17 14 cfv class f ⁡ a b
19 13 7 18 cmpt class b ∈ y ⟼ f ⁡ a b
20 12 6 19 cmpt class a ∈ x ⟼ b ∈ y ⟼ f ⁡ a b
21 5 11 20 cmpt class f ∈ x × y ⟶Set z ⟼ a ∈ x ⟼ b ∈ y ⟼ f ⁡ a b
22 1 3 4 2 2 2 21 cmpt3 class x ∈ V , y ∈ V , z ∈ V ⟼ f ∈ x × y ⟶Set z ⟼ a ∈ x ⟼ b ∈ y ⟼ f ⁡ a b
23 0 22 wceq wff curry_ = x ∈ V , y ∈ V , z ∈ V ⟼ f ∈ x × y ⟶Set z ⟼ a ∈ x ⟼ b ∈ y ⟼ f ⁡ a b