Theorem preddif

Description: Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011)

	Ref	Expression
Assertion	preddif	$$⊢Pred\left(R,\left(A\setminus B\right),X\right)=Pred\left(R,A,X\right)\setminus Pred\left(R,B,X\right)$$

Proof

Step	Hyp	Ref	Expression
1		indifdir	$$⊢\left(A\setminus B\right)\cap R^{-1}\left[\left\{X\right\}\right]=\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\setminus \left(B\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
2		df-pred	$$⊢Pred\left(R,\left(A\setminus B\right),X\right)=\left(A\setminus B\right)\cap R^{-1}\left[\left\{X\right\}\right]$$
3		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
4		df-pred	$$⊢Pred\left(R,B,X\right)=B\cap R^{-1}\left[\left\{X\right\}\right]$$
5	3 4	difeq12i	$$⊢Pred\left(R,A,X\right)\setminus Pred\left(R,B,X\right)=\left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\setminus \left(B\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
6	1 2 5	3eqtr4i	$$⊢Pred\left(R,\left(A\setminus B\right),X\right)=Pred\left(R,A,X\right)\setminus Pred\left(R,B,X\right)$$