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\in V\to Pred\left(R,A,N\right)=\left[N\right]{\left({R\upharpoonright }_A\right)}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		dfpred3g	$$⊢N\in V\to Pred\left(R,A,N\right)=\left\{m\in A|mRN\right\}$$
2		ec1cnvres	$$⊢N\in V\to \left[N\right]{\left({R\upharpoonright }_A\right)}^{-1}=\left\{m\in A|mRN\right\}$$
3	1 2	eqtr4d	$$⊢N\in V\to Pred\left(R,A,N\right)=\left[N\right]{\left({R\upharpoonright }_A\right)}^{-1}$$