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 
|- ( 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 ) )