Metamath Proof Explorer


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 }