Theorem dfrab3

Description: Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013)

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

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
2		inab	|- ( { x | x e. A } i^i { x | ph } ) = { x | ( x e. A /\ ph ) }
3		abid2	|- { x | x e. A } = A
4	3	ineq1i	|- ( { x | x e. A } i^i { x | ph } ) = ( A i^i { x | ph } )
5	1 2 4	3eqtr2i	|- { x e. A | ph } = ( A i^i { x | ph } )