Theorem mpteq12f

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013)

	Ref	Expression
Assertion	mpteq12f	⊢ ( ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝐴 = 𝐶
2		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷
3	1 2	nfan	⊢ Ⅎ 𝑥 ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 )
4		nfv	⊢ Ⅎ 𝑦 ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 )
5		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐷 )
6	5	eqeq2d	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝐵 ↔ 𝑦 = 𝐷 ) )
7	6	pm5.32da	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ) )
8		sp	⊢ ( ∀ 𝑥 𝐴 = 𝐶 → 𝐴 = 𝐶 )
9	8	eleq2d	⊢ ( ∀ 𝑥 𝐴 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶 ) )
10	9	anbi1d	⊢ ( ∀ 𝑥 𝐴 = 𝐶 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷 ) ) )
11	7 10	sylan9bbr	⊢ ( ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷 ) ) )
12	3 4 11	opabbid	⊢ ( ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷 ) } )
13		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
14		df-mpt	⊢ ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷 ) }
15	12 13 14	3eqtr4g	⊢ ( ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )