Metamath Proof Explorer

Theorem cbvmpo1davw2

Description: Change first bound variable and domains in a maps-to function. Deduction form. (Contributed by GG, 14-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 cbvmpo1davw2.1 ⊢ φ ∧ x = z → E = F
2 cbvmpo1davw2.2 ⊢ φ ∧ x = z → C = D
3 cbvmpo1davw2.3 ⊢ φ ∧ x = z → A = B
4 simpr ⊢ φ ∧ x = z → x = z
5 4 3 eleq12d ⊢ φ ∧ x = z → x ∈ A ↔ z ∈ B
6 2 eleq2d ⊢ φ ∧ x = z → y ∈ C ↔ y ∈ D
7 5 6 anbi12d ⊢ φ ∧ x = z → x ∈ A ∧ y ∈ C ↔ z ∈ B ∧ y ∈ D
8 1 eqeq2d ⊢ φ ∧ x = z → t = E ↔ t = F
9 7 8 anbi12d ⊢ φ ∧ x = z → x ∈ A ∧ y ∈ C ∧ t = E ↔ z ∈ B ∧ y ∈ D ∧ t = F
10 9 cbvoprab1davw ⊢ φ → x y t | x ∈ A ∧ y ∈ C ∧ t = E = z y t | z ∈ B ∧ y ∈ D ∧ t = F
11 df-mpo ⊢ x ∈ A , y ∈ C ⟼ E = x y t | x ∈ A ∧ y ∈ C ∧ t = E
12 df-mpo ⊢ z ∈ B , y ∈ D ⟼ F = z y t | z ∈ B ∧ y ∈ D ∧ t = F
13 10 11 12 3eqtr4g ⊢ φ → x ∈ A , y ∈ C ⟼ E = z ∈ B , y ∈ D ⟼ F