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

Metamath Proof Explorer

Theorem riinrab

Description: Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 riin0 
 |-  ( X = (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = A )
2 rzal 
 |-  ( X = (/) -> A. x e. X ph )
3 2 ralrimivw 
 |-  ( X = (/) -> A. y e. A A. x e. X ph )
4 rabid2 
 |-  ( A = { y e. A | A. x e. X ph } <-> A. y e. A A. x e. X ph )
5 3 4 sylibr 
 |-  ( X = (/) -> A = { y e. A | A. x e. X ph } )
6 1 5 eqtrd 
 |-  ( X = (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = { y e. A | A. x e. X ph } )
7 ssrab2 
 |-  { y e. A | ph } C_ A
8 7 rgenw 
 |-  A. x e. X { y e. A | ph } C_ A
9 riinn0 
 |-  ( ( A. x e. X { y e. A | ph } C_ A /\ X =/= (/) ) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = |^|_ x e. X { y e. A | ph } )
10 8 9 mpan 
 |-  ( X =/= (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = |^|_ x e. X { y e. A | ph } )
11 iinrab 
 |-  ( X =/= (/) -> |^|_ x e. X { y e. A | ph } = { y e. A | A. x e. X ph } )
12 10 11 eqtrd 
 |-  ( X =/= (/) -> ( A i^i |^|_ x e. X { y e. A | ph } ) = { y e. A | A. x e. X ph } )
13 6 12 pm2.61ine 
 |-  ( A i^i |^|_ x e. X { y e. A | ph } ) = { y e. A | A. x e. X ph }