This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ∀ 𝑥 𝐴 = 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐷 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )