# Metamath Proof Explorer

## Theorem cureq

Description: Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion cureq ${⊢}{A}={B}\to curry{A}=curry{B}$

### Proof

Step Hyp Ref Expression
1 dmeq ${⊢}{A}={B}\to \mathrm{dom}{A}=\mathrm{dom}{B}$
2 1 dmeqd ${⊢}{A}={B}\to \mathrm{dom}\mathrm{dom}{A}=\mathrm{dom}\mathrm{dom}{B}$
3 breq ${⊢}{A}={B}\to \left(⟨{x},{y}⟩{A}{z}↔⟨{x},{y}⟩{B}{z}\right)$
4 3 opabbidv ${⊢}{A}={B}\to \left\{⟨{y},{z}⟩|⟨{x},{y}⟩{A}{z}\right\}=\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{B}{z}\right\}$
5 2 4 mpteq12dv ${⊢}{A}={B}\to \left({x}\in \mathrm{dom}\mathrm{dom}{A}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{A}{z}\right\}\right)=\left({x}\in \mathrm{dom}\mathrm{dom}{B}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{B}{z}\right\}\right)$
6 df-cur ${⊢}curry{A}=\left({x}\in \mathrm{dom}\mathrm{dom}{A}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{A}{z}\right\}\right)$
7 df-cur ${⊢}curry{B}=\left({x}\in \mathrm{dom}\mathrm{dom}{B}⟼\left\{⟨{y},{z}⟩|⟨{x},{y}⟩{B}{z}\right\}\right)$
8 5 6 7 3eqtr4g ${⊢}{A}={B}\to curry{A}=curry{B}$