Theorem unceq

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

	Ref	Expression
Assertion	unceq	⊢ ( 𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ‘ 𝑥 ) = ( 𝐵 ‘ 𝑥 ) )
2	1	breqd	⊢ ( 𝐴 = 𝐵 → ( 𝑦 ( 𝐴 ‘ 𝑥 ) 𝑧 ↔ 𝑦 ( 𝐵 ‘ 𝑥 ) 𝑧 ) )
3	2	oprabbidv	⊢ ( 𝐴 = 𝐵 → { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐴 ‘ 𝑥 ) 𝑧 } = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐵 ‘ 𝑥 ) 𝑧 } )
4		df-unc	⊢ uncurry 𝐴 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐴 ‘ 𝑥 ) 𝑧 }
5		df-unc	⊢ uncurry 𝐵 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝑦 ( 𝐵 ‘ 𝑥 ) 𝑧 }
6	3 4 5	3eqtr4g	⊢ ( 𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵 )