Theorem inrab2

Description: Intersection with a restricted class abstraction. (Contributed by NM, 19-Nov-2007)

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		abid1	|- B = { x | x e. B }
3	1 2	ineq12i	|- ( { x e. A | ph } i^i B ) = ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } )
4		df-rab	|- { x e. ( A i^i B ) | ph } = { x | ( x e. ( A i^i B ) /\ ph ) }
5		inab	|- ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } ) = { x | ( ( x e. A /\ ph ) /\ x e. B ) }
6		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
7	6	anbi1i	|- ( ( x e. ( A i^i B ) /\ ph ) <-> ( ( x e. A /\ x e. B ) /\ ph ) )
8		an32	|- ( ( ( x e. A /\ x e. B ) /\ ph ) <-> ( ( x e. A /\ ph ) /\ x e. B ) )
9	7 8	bitri	|- ( ( x e. ( A i^i B ) /\ ph ) <-> ( ( x e. A /\ ph ) /\ x e. B ) )
10	9	abbii	|- { x | ( x e. ( A i^i B ) /\ ph ) } = { x | ( ( x e. A /\ ph ) /\ x e. B ) }
11	5 10	eqtr4i	|- ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } ) = { x | ( x e. ( A i^i B ) /\ ph ) }
12	4 11	eqtr4i	|- { x e. ( A i^i B ) | ph } = ( { x | ( x e. A /\ ph ) } i^i { x | x e. B } )
13	3 12	eqtr4i	|- ( { x e. A | ph } i^i B ) = { x e. ( A i^i B ) | ph }