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

Metamath Proof Explorer

Theorem iinrab2

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

Ref Expression
Assertion iinrab2 
|- ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph }

Proof

Step Hyp Ref Expression
1 iineq1 
 |-  ( A = (/) -> |^|_ x e. A { y e. B | ph } = |^|_ x e. (/) { y e. B | ph } )
2 0iin 
 |-  |^|_ x e. (/) { y e. B | ph } = _V
3 1 2 eqtrdi 
 |-  ( A = (/) -> |^|_ x e. A { y e. B | ph } = _V )
4 3 ineq1d 
 |-  ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = ( _V i^i B ) )
5 incom 
 |-  ( _V i^i B ) = ( B i^i _V )
6 inv1 
 |-  ( B i^i _V ) = B
7 5 6 eqtri 
 |-  ( _V i^i B ) = B
8 4 7 eqtrdi 
 |-  ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = B )
9 rzal 
 |-  ( A = (/) -> A. x e. A A. y e. B ph )
10 rabid2 
 |-  ( B = { y e. B | A. x e. A ph } <-> A. y e. B A. x e. A ph )
11 ralcom 
 |-  ( A. y e. B A. x e. A ph <-> A. x e. A A. y e. B ph )
12 10 11 bitr2i 
 |-  ( A. x e. A A. y e. B ph <-> B = { y e. B | A. x e. A ph } )
13 9 12 sylib 
 |-  ( A = (/) -> B = { y e. B | A. x e. A ph } )
14 8 13 eqtrd 
 |-  ( A = (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph } )
15 iinrab 
 |-  ( A =/= (/) -> |^|_ x e. A { y e. B | ph } = { y e. B | A. x e. A ph } )
16 15 ineq1d 
 |-  ( A =/= (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = ( { y e. B | A. x e. A ph } i^i B ) )
17 ssrab2 
 |-  { y e. B | A. x e. A ph } C_ B
18 dfss 
 |-  ( { y e. B | A. x e. A ph } C_ B <-> { y e. B | A. x e. A ph } = ( { y e. B | A. x e. A ph } i^i B ) )
19 17 18 mpbi 
 |-  { y e. B | A. x e. A ph } = ( { y e. B | A. x e. A ph } i^i B )
20 16 19 eqtr4di 
 |-  ( A =/= (/) -> ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph } )
21 14 20 pm2.61ine 
 |-  ( |^|_ x e. A { y e. B | ph } i^i B ) = { y e. B | A. x e. A ph }