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	⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 ) → ∩ 𝑥 ∈ 𝐴 𝐶 = ∩ 𝑥 ∈ 𝐵 𝐷 )