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 } |
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 } |