Metamath Proof Explorer


Theorem iineq12f

Description: Equality deduction for indexed intersections. (Contributed by Giovanni Mascellani, 10-Apr-2018)

Ref Expression
Hypotheses iineq12f.1 𝑥 𝐴
iineq12f.2 𝑥 𝐵
Assertion iineq12f ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥𝐴 𝐶 = 𝐷 ) → 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 iineq12f.1 𝑥 𝐴
2 iineq12f.2 𝑥 𝐵
3 eleq2 ( 𝐶 = 𝐷 → ( 𝑦𝐶𝑦𝐷 ) )
4 3 ralimi ( ∀ 𝑥𝐴 𝐶 = 𝐷 → ∀ 𝑥𝐴 ( 𝑦𝐶𝑦𝐷 ) )
5 ralbi ( ∀ 𝑥𝐴 ( 𝑦𝐶𝑦𝐷 ) → ( ∀ 𝑥𝐴 𝑦𝐶 ↔ ∀ 𝑥𝐴 𝑦𝐷 ) )
6 4 5 syl ( ∀ 𝑥𝐴 𝐶 = 𝐷 → ( ∀ 𝑥𝐴 𝑦𝐶 ↔ ∀ 𝑥𝐴 𝑦𝐷 ) )
7 1 2 raleqf ( 𝐴 = 𝐵 → ( ∀ 𝑥𝐴 𝑦𝐷 ↔ ∀ 𝑥𝐵 𝑦𝐷 ) )
8 6 7 sylan9bbr ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥𝐴 𝐶 = 𝐷 ) → ( ∀ 𝑥𝐴 𝑦𝐶 ↔ ∀ 𝑥𝐵 𝑦𝐷 ) )
9 8 abbidv ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥𝐴 𝐶 = 𝐷 ) → { 𝑦 ∣ ∀ 𝑥𝐴 𝑦𝐶 } = { 𝑦 ∣ ∀ 𝑥𝐵 𝑦𝐷 } )
10 df-iin 𝑥𝐴 𝐶 = { 𝑦 ∣ ∀ 𝑥𝐴 𝑦𝐶 }
11 df-iin 𝑥𝐵 𝐷 = { 𝑦 ∣ ∀ 𝑥𝐵 𝑦𝐷 }
12 9 10 11 3eqtr4g ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥𝐴 𝐶 = 𝐷 ) → 𝑥𝐴 𝐶 = 𝑥𝐵 𝐷 )