Metamath Proof Explorer

Theorem dfpred4

Description: Alternate definition of the predecessor class when N is a set. (Contributed by Peter Mazsa, 26-Jan-2026)

Ref Expression
Assertion dfpred4 
|- ( N e. V -> Pred ( R , A , N ) = [ N ] `' ( R |` A ) )

Proof

Step Hyp Ref Expression
1 dfpred3g 
 |-  ( N e. V -> Pred ( R , A , N ) = { m e. A | m R N } )
2 ec1cnvres 
 |-  ( N e. V -> [ N ] `' ( R |` A ) = { m e. A | m R N } )
3 1 2 eqtr4d 
 |-  ( N e. V -> Pred ( R , A , N ) = [ N ] `' ( R |` A ) )