Theorem dfpred2

Description: An alternate definition of predecessor class when X is a set. (Contributed by Scott Fenton, 8-Feb-2011)

	Ref	Expression
Hypothesis	dfpred2.1	|- X e. _V
Assertion	dfpred2	|- Pred ( R , A , X ) = ( A i^i { y | y R X } )

Proof

Step	Hyp	Ref	Expression
1		dfpred2.1	|- X e. _V
2		df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
3		iniseg	|- ( X e. _V -> ( `' R " { X } ) = { y | y R X } )
4	1 3	ax-mp	|- ( `' R " { X } ) = { y | y R X }
5	4	ineq2i	|- ( A i^i ( `' R " { X } ) ) = ( A i^i { y | y R X } )
6	2 5	eqtri	|- Pred ( R , A , X ) = ( A i^i { y | y R X } )