Metamath Proof Explorer

Theorem cbvixp

Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011)

Ref Expression
Hypotheses cbvixp.1 ⊢ Ⅎ _ y B
cbvixp.2 ⊢ Ⅎ _ x C
cbvixp.3 ⊢ x = y → B = C
Assertion cbvixp ⊢ ⨉ x ∈ A B = ⨉ y ∈ A C

Proof

Step Hyp Ref Expression
1 cbvixp.1 ⊢ Ⅎ _ y B
2 cbvixp.2 ⊢ Ⅎ _ x C
3 cbvixp.3 ⊢ x = y → B = C
4 1 nfel2 ⊢ Ⅎ y f ⁡ x ∈ B
5 2 nfel2 ⊢ Ⅎ x f ⁡ y ∈ C
6 fveq2 ⊢ x = y → f ⁡ x = f ⁡ y
7 6 3 eleq12d ⊢ x = y → f ⁡ x ∈ B ↔ f ⁡ y ∈ C
8 4 5 7 cbvralw ⊢ ∀ x ∈ A f ⁡ x ∈ B ↔ ∀ y ∈ A f ⁡ y ∈ C
9 8 anbi2i ⊢ f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B ↔ f Fn A ∧ ∀ y ∈ A f ⁡ y ∈ C
10 9 abbii ⊢ f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B = f | f Fn A ∧ ∀ y ∈ A f ⁡ y ∈ C
11 dfixp ⊢ ⨉ x ∈ A B = f | f Fn A ∧ ∀ x ∈ A f ⁡ x ∈ B
12 dfixp ⊢ ⨉ y ∈ A C = f | f Fn A ∧ ∀ y ∈ A f ⁡ y ∈ C
13 10 11 12 3eqtr4i ⊢ ⨉ x ∈ A B = ⨉ y ∈ A C