Theorem cureq

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

	Ref	Expression
Assertion	cureq	⊢ ( 𝐴 = 𝐵 → curry 𝐴 = curry 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dmeq	⊢ ( 𝐴 = 𝐵 → dom 𝐴 = dom 𝐵 )
2	1	dmeqd	⊢ ( 𝐴 = 𝐵 → dom dom 𝐴 = dom dom 𝐵 )
3		breq	⊢ ( 𝐴 = 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ 𝐴 𝑧 ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝐵 𝑧 ) )
4	3	opabbidv	⊢ ( 𝐴 = 𝐵 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐴 𝑧 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐵 𝑧 } )
5	2 4	mpteq12dv	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ dom dom 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐴 𝑧 } ) = ( 𝑥 ∈ dom dom 𝐵 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐵 𝑧 } ) )
6		df-cur	⊢ curry 𝐴 = ( 𝑥 ∈ dom dom 𝐴 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐴 𝑧 } )
7		df-cur	⊢ curry 𝐵 = ( 𝑥 ∈ dom dom 𝐵 ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ 𝐵 𝑧 } )
8	5 6 7	3eqtr4g	⊢ ( 𝐴 = 𝐵 → curry 𝐴 = curry 𝐵 )