Metamath Proof Explorer

Theorem mpoeq123dva

Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses mpoeq123dv.1 ⊢ φ → A = D
mpoeq123dva.2 ⊢ φ ∧ x ∈ A → B = E
mpoeq123dva.3 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C = F
Assertion mpoeq123dva ⊢ φ → x ∈ A , y ∈ B ⟼ C = x ∈ D , y ∈ E ⟼ F

Proof

Step Hyp Ref Expression
1 mpoeq123dv.1 ⊢ φ → A = D
2 mpoeq123dva.2 ⊢ φ ∧ x ∈ A → B = E
3 mpoeq123dva.3 ⊢ φ ∧ x ∈ A ∧ y ∈ B → C = F
4 3 eqeq2d ⊢ φ ∧ x ∈ A ∧ y ∈ B → z = C ↔ z = F
5 4 pm5.32da ⊢ φ → x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ A ∧ y ∈ B ∧ z = F
6 2 eleq2d ⊢ φ ∧ x ∈ A → y ∈ B ↔ y ∈ E
7 6 pm5.32da ⊢ φ → x ∈ A ∧ y ∈ B ↔ x ∈ A ∧ y ∈ E
8 1 eleq2d ⊢ φ → x ∈ A ↔ x ∈ D
9 8 anbi1d ⊢ φ → x ∈ A ∧ y ∈ E ↔ x ∈ D ∧ y ∈ E
10 7 9 bitrd ⊢ φ → x ∈ A ∧ y ∈ B ↔ x ∈ D ∧ y ∈ E
11 10 anbi1d ⊢ φ → x ∈ A ∧ y ∈ B ∧ z = F ↔ x ∈ D ∧ y ∈ E ∧ z = F
12 5 11 bitrd ⊢ φ → x ∈ A ∧ y ∈ B ∧ z = C ↔ x ∈ D ∧ y ∈ E ∧ z = F
13 12 oprabbidv ⊢ φ → x y z | x ∈ A ∧ y ∈ B ∧ z = C = x y z | x ∈ D ∧ y ∈ E ∧ z = F
14 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C
15 df-mpo ⊢ x ∈ D , y ∈ E ⟼ F = x y z | x ∈ D ∧ y ∈ E ∧ z = F
16 13 14 15 3eqtr4g ⊢ φ → x ∈ A , y ∈ B ⟼ C = x ∈ D , y ∈ E ⟼ F