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

Metamath Proof Explorer

Theorem iinrab

Description: Indexed intersection of a restricted class abstraction. (Contributed by NM, 6-Dec-2011)

Ref Expression
Assertion iinrab 
|- ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )

Proof

Step Hyp Ref Expression
1 r19.28zv 
 |-  ( A =/= (/) -> ( A. x e. A ( y e. B /\ ph ) <-> ( y e. B /\ A. x e. A ph ) ) )
2 1 abbidv 
 |-  ( A =/= (/) -> { y | A. x e. A ( y e. B /\ ph ) } = { y | ( y e. B /\ A. x e. A ph ) } )
3 df-rab 
 |-  { y e. B | ph } = { y | ( y e. B /\ ph ) }
4 3 a1i 
 |-  ( x e. A -> { y e. B | ph } = { y | ( y e. B /\ ph ) } )
5 4 iineq2i 
 |-  |^|_ x e. A { y e. B | ph } = |^|_ x e. A { y | ( y e. B /\ ph ) }
6 iinab 
 |-  |^|_ x e. A { y | ( y e. B /\ ph ) } = { y | A. x e. A ( y e. B /\ ph ) }
7 5 6 eqtri 
 |-  |^|_ x e. A { y e. B | ph } = { y | A. x e. A ( y e. B /\ ph ) }
8 df-rab 
 |-  { y e. B | A. x e. A ph } = { y | ( y e. B /\ A. x e. A ph ) }
9 2 7 8 3eqtr4g 
 |-  ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )