Metamath Proof Explorer

Theorem cbvixpdavw2

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

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

Proof

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