Description: Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | iineq2 | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 | ⊢ ( 𝐵 = 𝐶 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) | |
2 | 1 | ralimi | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) ) |
3 | ralbi | ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) ) | |
4 | 2 3 | syl | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ) ) |
5 | 4 | abbidv | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 } ) |
6 | df-iin | ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } | |
7 | df-iin | ⊢ ∩ 𝑥 ∈ 𝐴 𝐶 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 } | |
8 | 5 6 7 | 3eqtr4g | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 𝐶 ) |