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 }