Metamath Proof Explorer

Theorem cbvmptdavw2

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

Ref Expression
Hypotheses cbvmptdavw2.1 ⊢ φ ∧ x = y → C = D
cbvmptdavw2.2 ⊢ φ ∧ x = y → A = B
Assertion cbvmptdavw2 ⊢ φ → x ∈ A ⟼ C = y ∈ B ⟼ D

Proof

Step Hyp Ref Expression
1 cbvmptdavw2.1 ⊢ φ ∧ x = y → C = D
2 cbvmptdavw2.2 ⊢ φ ∧ x = y → A = B
3 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
4 3 adantl ⊢ φ ∧ x = y → x ∈ A ↔ y ∈ A
5 2 eleq2d ⊢ φ ∧ x = y → y ∈ A ↔ y ∈ B
6 4 5 bitrd ⊢ φ ∧ x = y → x ∈ A ↔ y ∈ B
7 1 eqeq2d ⊢ φ ∧ x = y → t = C ↔ t = D
8 6 7 anbi12d ⊢ φ ∧ x = y → x ∈ A ∧ t = C ↔ y ∈ B ∧ t = D
9 8 cbvopab1davw ⊢ φ → x t | x ∈ A ∧ t = C = y t | y ∈ B ∧ t = D
10 df-mpt ⊢ x ∈ A ⟼ C = x t | x ∈ A ∧ t = C
11 df-mpt ⊢ y ∈ B ⟼ D = y t | y ∈ B ∧ t = D
12 9 10 11 3eqtr4g ⊢ φ → x ∈ A ⟼ C = y ∈ B ⟼ D