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	⊢ ( 𝑁 ∈ 𝑉 → Pred ( 𝑅 , 𝐴 , 𝑁 ) = [ 𝑁 ] ◡ ( 𝑅 ↾ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfpred3g	⊢ ( 𝑁 ∈ 𝑉 → Pred ( 𝑅 , 𝐴 , 𝑁 ) = { 𝑚 ∈ 𝐴 ∣ 𝑚 𝑅 𝑁 } )
2		ec1cnvres	⊢ ( 𝑁 ∈ 𝑉 → [ 𝑁 ] ◡ ( 𝑅 ↾ 𝐴 ) = { 𝑚 ∈ 𝐴 ∣ 𝑚 𝑅 𝑁 } )
3	1 2	eqtr4d	⊢ ( 𝑁 ∈ 𝑉 → Pred ( 𝑅 , 𝐴 , 𝑁 ) = [ 𝑁 ] ◡ ( 𝑅 ↾ 𝐴 ) )