Theorem iinxprg

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

	Ref	Expression
Hypotheses	iinxprg.1	|- ( x = A -> C = D )
	iinxprg.2	|- ( x = B -> C = E )
Assertion	iinxprg	|- ( ( A e. V /\ B e. W ) -> |^|_ x e. { A , B } C = ( D i^i E ) )

Proof

Step	Hyp	Ref	Expression
1		iinxprg.1	|- ( x = A -> C = D )
2		iinxprg.2	|- ( x = B -> C = E )
3	1	eleq2d	|- ( x = A -> ( y e. C <-> y e. D ) )
4	2	eleq2d	|- ( x = B -> ( y e. C <-> y e. E ) )
5	3 4	ralprg	|- ( ( A e. V /\ B e. W ) -> ( A. x e. { A , B } y e. C <-> ( y e. D /\ y e. E ) ) )
6	5	abbidv	|- ( ( A e. V /\ B e. W ) -> { y | A. x e. { A , B } y e. C } = { y | ( y e. D /\ y e. E ) } )
7		df-iin	|- |^|_ x e. { A , B } C = { y | A. x e. { A , B } y e. C }
8		df-in	|- ( D i^i E ) = { y | ( y e. D /\ y e. E ) }
9	6 7 8	3eqtr4g	|- ( ( A e. V /\ B e. W ) -> |^|_ x e. { A , B } C = ( D i^i E ) )