This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∩ 𝑥 ∈ { 𝐴 , 𝐵 } 𝐶 = ( 𝐷 ∩ 𝐸 ) )