Theorem dfpred3

Description: An alternate definition of predecessor class when X is a set. (Contributed by Scott Fenton, 13-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		dfpred2.1	|- X e. _V
2		incom	|- ( A i^i { y | y R X } ) = ( { y | y R X } i^i A )
3	1	dfpred2	|- Pred ( R , A , X ) = ( A i^i { y | y R X } )
4		dfrab2	|- { y e. A | y R X } = ( { y | y R X } i^i A )
5	2 3 4	3eqtr4i	|- Pred ( R , A , X ) = { y e. A | y R X }