Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-unc | Structured version Visualization version GIF version |
Description: Define the uncurrying of 𝐹, which takes a function producing functions, and transforms it into a two-argument function. (Contributed by Mario Carneiro, 7-Jan-2017.) |
Ref | Expression |
---|---|
df-unc | ⊢ uncurry 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cF | . . 3 class 𝐹 | |
2 | 1 | cunc 8008 | . 2 class uncurry 𝐹 |
3 | vy | . . . . 5 setvar 𝑦 | |
4 | 3 | cv 1542 | . . . 4 class 𝑦 |
5 | vz | . . . . 5 setvar 𝑧 | |
6 | 5 | cv 1542 | . . . 4 class 𝑧 |
7 | vx | . . . . . 6 setvar 𝑥 | |
8 | 7 | cv 1542 | . . . . 5 class 𝑥 |
9 | 8, 1 | cfv 6380 | . . . 4 class (𝐹‘𝑥) |
10 | 4, 6, 9 | wbr 5053 | . . 3 wff 𝑦(𝐹‘𝑥)𝑧 |
11 | 10, 7, 3, 5 | coprab 7214 | . 2 class {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧} |
12 | 2, 11 | wceq 1543 | 1 wff uncurry 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑦(𝐹‘𝑥)𝑧} |
Colors of variables: wff setvar class |
This definition is referenced by: unceq 35491 uncf 35493 uncov 35495 unccur 35497 |
Copyright terms: Public domain | W3C validator |