Metamath Proof Explorer

Theorem cbvmpo2davw2

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

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

Proof

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