Theorem pred0

Description: The predecessor class over (/) is always (/) . (Contributed by Scott Fenton, 16-Apr-2011) (Proof shortened by AV, 11-Jun-2021)

	Ref	Expression
Assertion	pred0	$$⊢Pred\left(R,\varnothing ,X\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-pred	$$⊢Pred\left(R,\varnothing ,X\right)=\varnothing \cap R^{-1}\left[\left\{X\right\}\right]$$
2		0in	$$⊢\varnothing \cap R^{-1}\left[\left\{X\right\}\right]=\varnothing$$
3	1 2	eqtri	$$⊢Pred\left(R,\varnothing ,X\right)=\varnothing$$