Theorem predprc

Description: The predecessor of a proper class is empty. (Contributed by Scott Fenton, 25-Nov-2024)

	Ref	Expression
Assertion	predprc	$$⊢\neg X\in \mathrm{V}\to Pred\left(R,A,X\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
2		snprc	$$⊢\neg X\in \mathrm{V}\leftrightarrow \left\{X\right\}=\varnothing$$
3	2	biimpi	$$⊢\neg X\in \mathrm{V}\to \left\{X\right\}=\varnothing$$
4	3	imaeq2d	$$⊢\neg X\in \mathrm{V}\to R^{-1}\left[\left\{X\right\}\right]=R^{-1}\left[\varnothing \right]$$
5		ima0	$$⊢R^{-1}\left[\varnothing \right]=\varnothing$$
6	4 5	eqtrdi	$$⊢\neg X\in \mathrm{V}\to R^{-1}\left[\left\{X\right\}\right]=\varnothing$$
7	6	ineq2d	$$⊢\neg X\in \mathrm{V}\to A\cap R^{-1}\left[\left\{X\right\}\right]=A\cap \varnothing$$
8		in0	$$⊢A\cap \varnothing =\varnothing$$
9	7 8	eqtrdi	$$⊢\neg X\in \mathrm{V}\to A\cap R^{-1}\left[\left\{X\right\}\right]=\varnothing$$
10	1 9	eqtrid	$$⊢\neg X\in \mathrm{V}\to Pred\left(R,A,X\right)=\varnothing$$