Theorem dfpred3g

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

	Ref	Expression
Assertion	dfpred3g	|- ( X e. V -> Pred ( R , A , X ) = { y e. A | y R X } )

Proof

Step	Hyp	Ref	Expression
1		predeq3	|- ( x = X -> Pred ( R , A , x ) = Pred ( R , A , X ) )
2		breq2	|- ( x = X -> ( y R x <-> y R X ) )
3	2	rabbidv	|- ( x = X -> { y e. A | y R x } = { y e. A | y R X } )
4	1 3	eqeq12d	|- ( x = X -> ( Pred ( R , A , x ) = { y e. A | y R x } <-> Pred ( R , A , X ) = { y e. A | y R X } ) )
5		vex	|- x e. _V
6	5	dfpred3	|- Pred ( R , A , x ) = { y e. A | y R x }
7	4 6	vtoclg	|- ( X e. V -> Pred ( R , A , X ) = { y e. A | y R X } )