Metamath Proof Explorer

Theorem cbvixpdavw

Description: Change bound variable in an indexed Cartesian product. Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypothesis cbvixpdavw.1 ⊢ φ ∧ x = y → B = C
Assertion cbvixpdavw ⊢ φ → ⨉ x ∈ A B = ⨉ y ∈ A C

Proof

Step Hyp Ref Expression
1 cbvixpdavw.1 ⊢ φ ∧ x = y → B = C
2 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
3 2 adantl ⊢ φ ∧ x = y → x ∈ A ↔ y ∈ A
4 3 cbvabdavw ⊢ φ → x | x ∈ A = y | y ∈ A
5 4 fneq2d ⊢ φ → t Fn x | x ∈ A ↔ t Fn y | y ∈ A
6 simpr ⊢ φ ∧ x = y → x = y
7 6 fveq2d ⊢ φ ∧ x = y → t ⁡ x = t ⁡ y
8 7 1 eleq12d ⊢ φ ∧ x = y → t ⁡ x ∈ B ↔ t ⁡ y ∈ C
9 8 cbvraldva ⊢ φ → ∀ x ∈ A t ⁡ x ∈ B ↔ ∀ y ∈ A t ⁡ y ∈ C
10 5 9 anbi12d ⊢ φ → t Fn x | x ∈ A ∧ ∀ x ∈ A t ⁡ x ∈ B ↔ t Fn y | y ∈ A ∧ ∀ y ∈ A t ⁡ y ∈ C
11 10 abbidv ⊢ φ → t | t Fn x | x ∈ A ∧ ∀ x ∈ A t ⁡ x ∈ B = t | t Fn y | y ∈ A ∧ ∀ y ∈ A t ⁡ y ∈ C
12 df-ixp ⊢ ⨉ x ∈ A B = t | t Fn x | x ∈ A ∧ ∀ x ∈ A t ⁡ x ∈ B
13 df-ixp ⊢ ⨉ y ∈ A C = t | t Fn y | y ∈ A ∧ ∀ y ∈ A t ⁡ y ∈ C
14 11 12 13 3eqtr4g ⊢ φ → ⨉ x ∈ A B = ⨉ y ∈ A C