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 ⊢ ∀ x A = C ∧ ∀ x ∈ A B = D → x ∈ A ⟼ B = x ∈ C ⟼ D

Proof

Step Hyp Ref Expression
1 nfa1 ⊢ Ⅎ x ∀ x A = C
2 nfra1 ⊢ Ⅎ x ∀ x ∈ A B = D
3 1 2 nfan ⊢ Ⅎ x ∀ x A = C ∧ ∀ x ∈ A B = D
4 nfv ⊢ Ⅎ y ∀ x A = C ∧ ∀ x ∈ A B = D
5 rspa ⊢ ∀ x ∈ A B = D ∧ x ∈ A → B = D
6 5 eqeq2d ⊢ ∀ x ∈ A B = D ∧ x ∈ A → y = B ↔ y = D
7 6 pm5.32da ⊢ ∀ x ∈ A B = D → x ∈ A ∧ y = B ↔ x ∈ A ∧ y = D
8 sp ⊢ ∀ x A = C → A = C
9 8 eleq2d ⊢ ∀ x A = C → x ∈ A ↔ x ∈ C
10 9 anbi1d ⊢ ∀ x A = C → x ∈ A ∧ y = D ↔ x ∈ C ∧ y = D
11 7 10 sylan9bbr ⊢ ∀ x A = C ∧ ∀ x ∈ A B = D → x ∈ A ∧ y = B ↔ x ∈ C ∧ y = D
12 3 4 11 opabbid ⊢ ∀ x A = C ∧ ∀ x ∈ A B = D → x y | x ∈ A ∧ y = B = x y | x ∈ C ∧ y = D
13 df-mpt ⊢ x ∈ A ⟼ B = x y | x ∈ A ∧ y = B
14 df-mpt ⊢ x ∈ C ⟼ D = x y | x ∈ C ∧ y = D
15 12 13 14 3eqtr4g ⊢ ∀ x A = C ∧ ∀ x ∈ A B = D → x ∈ A ⟼ B = x ∈ C ⟼ D