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 }