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\leftrightarrow y\in D\right)$$
4	2	eleq2d	$$⊢x=B\to \left(y\in C\leftrightarrow 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\}y\in C\leftrightarrow \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\}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\}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$$