Theorem cureq

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

	Ref	Expression
Assertion	cureq	$$⊢A=B\to curryA=curryB$$

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⟩Az\leftrightarrow ⟨x,y⟩Bz\right)$$
4	3	opabbidv	$$⊢A=B\to \left\{⟨y,z⟩|⟨x,y⟩Az\right\}=\left\{⟨y,z⟩|⟨x,y⟩Bz\right\}$$
5	2 4	mpteq12dv	$$⊢A=B\to \left(x\in \mathrm{dom}\mathrm{dom}A⟼\left\{⟨y,z⟩|⟨x,y⟩Az\right\}\right)=\left(x\in \mathrm{dom}\mathrm{dom}B⟼\left\{⟨y,z⟩|⟨x,y⟩Bz\right\}\right)$$
6		df-cur	$$⊢curryA=\left(x\in \mathrm{dom}\mathrm{dom}A⟼\left\{⟨y,z⟩|⟨x,y⟩Az\right\}\right)$$
7		df-cur	$$⊢curryB=\left(x\in \mathrm{dom}\mathrm{dom}B⟼\left\{⟨y,z⟩|⟨x,y⟩Bz\right\}\right)$$
8	5 6 7	3eqtr4g	$$⊢A=B\to curryA=curryB$$