Theorem unceq

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

	Ref	Expression
Assertion	unceq	|- ( A = B -> uncurry A = uncurry B )

Proof

Step	Hyp	Ref	Expression
1		fveq1	|- ( A = B -> ( A ` x ) = ( B ` x ) )
2	1	breqd	|- ( A = B -> ( y ( A ` x ) z <-> y ( B ` x ) z ) )
3	2	oprabbidv	|- ( A = B -> { <. <. x , y >. , z >. | y ( A ` x ) z } = { <. <. x , y >. , z >. | y ( B ` x ) z } )
4		df-unc	|- uncurry A = { <. <. x , y >. , z >. | y ( A ` x ) z }
5		df-unc	|- uncurry B = { <. <. x , y >. , z >. | y ( B ` x ) z }
6	3 4 5	3eqtr4g	|- ( A = B -> uncurry A = uncurry B )