Theorem cureq

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

	Ref	Expression
Assertion	cureq	|- ( A = B -> curry A = curry B )

Proof

Step	Hyp	Ref	Expression
1		dmeq	|- ( A = B -> dom A = dom B )
2	1	dmeqd	|- ( A = B -> dom dom A = dom dom B )
3		breq	|- ( A = B -> ( <. x , y >. A z <-> <. x , y >. B z ) )
4	3	opabbidv	|- ( A = B -> { <. y , z >. | <. x , y >. A z } = { <. y , z >. | <. x , y >. B z } )
5	2 4	mpteq12dv	|- ( A = B -> ( x e. dom dom A |-> { <. y , z >. | <. x , y >. A z } ) = ( x e. dom dom B |-> { <. y , z >. | <. x , y >. B z } ) )
6		df-cur	|- curry A = ( x e. dom dom A |-> { <. y , z >. | <. x , y >. A z } )
7		df-cur	|- curry B = ( x e. dom dom B |-> { <. y , z >. | <. x , y >. B z } )
8	5 6 7	3eqtr4g	|- ( A = B -> curry A = curry B )