Description: Change bound variables in an indexed intersection. (Contributed by Jeff Hankins, 26-Aug-2009) Add disjoint variable condition to avoid ax-13 . See cbviinvg for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbviunv.1 | ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 ) | |
| Assertion | cbviinv | ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbviunv.1 | ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 ) | |
| 2 | 1 | eleq2d | ⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶 ) ) |
| 3 | 2 | cbvralvw | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 ) |
| 4 | 3 | abbii | ⊢ { 𝑧 ∣ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } = { 𝑧 ∣ ∀ 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 } |
| 5 | df-iin | ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ∀ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 } | |
| 6 | df-iin | ⊢ ∩ 𝑦 ∈ 𝐴 𝐶 = { 𝑧 ∣ ∀ 𝑦 ∈ 𝐴 𝑧 ∈ 𝐶 } | |
| 7 | 4 5 6 | 3eqtr4i | ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑦 ∈ 𝐴 𝐶 |