Theorem iinxprg

Description: Indexed intersection with an unordered pair index. (Contributed by NM, 25-Jan-2012)

	Ref	Expression
Hypotheses	iinxprg.1	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
	iinxprg.2	⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
Assertion	iinxprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 ∩ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		iinxprg.1	⊢ ( 𝑥 = 𝐴 → 𝐶 = 𝐷 )
2		iinxprg.2	⊢ ( 𝑥 = 𝐵 → 𝐶 = 𝐸 )
3	1	eleq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
4	2	eleq2d	⊢ ( 𝑥 = 𝐵 → ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐸 ) )
5	3 4	ralprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑦 ∈ 𝐶 ↔ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) ) )
6	5	abbidv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝑦 ∣ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑦 ∈ 𝐶 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) } )
7		df-iin	⊢ ∩ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = { 𝑦 ∣ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑦 ∈ 𝐶 }
8		df-in	⊢ ( 𝐷 ∩ 𝐸 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐷 ∧ 𝑦 ∈ 𝐸 ) }
9	6 7 8	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 ∩ 𝐸 ) )