Metamath Proof Explorer


Theorem iineq2

Description: Equality theorem for indexed intersection. (Contributed by NM, 22-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion iineq2 ( ∀ 𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶 )

Proof

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 ( ∀ 𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶 )