# Metamath Proof Explorer

## Theorem iinxprg

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

Ref Expression
Hypotheses iinxprg.1 ${⊢}{x}={A}\to {C}={D}$
iinxprg.2 ${⊢}{x}={B}\to {C}={E}$
Assertion iinxprg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \bigcap _{{x}\in \left\{{A},{B}\right\}}{C}={D}\cap {E}$

### Proof

Step Hyp Ref Expression
1 iinxprg.1 ${⊢}{x}={A}\to {C}={D}$
2 iinxprg.2 ${⊢}{x}={B}\to {C}={E}$
3 1 eleq2d ${⊢}{x}={A}\to \left({y}\in {C}↔{y}\in {D}\right)$
4 2 eleq2d ${⊢}{x}={B}\to \left({y}\in {C}↔{y}\in {E}\right)$
5 3 4 ralprg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(\forall {x}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}{y}\in {C}↔\left({y}\in {D}\wedge {y}\in {E}\right)\right)$
6 5 abbidv ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left\{{y}|\forall {x}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right\}=\left\{{y}|\left({y}\in {D}\wedge {y}\in {E}\right)\right\}$
7 df-iin ${⊢}\bigcap _{{x}\in \left\{{A},{B}\right\}}{C}=\left\{{y}|\forall {x}\in \left\{{A},{B}\right\}\phantom{\rule{.4em}{0ex}}{y}\in {C}\right\}$
8 df-in ${⊢}{D}\cap {E}=\left\{{y}|\left({y}\in {D}\wedge {y}\in {E}\right)\right\}$
9 6 7 8 3eqtr4g ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \bigcap _{{x}\in \left\{{A},{B}\right\}}{C}={D}\cap {E}$