Theorem csbpredg

Description: Move class substitution in and out of the predecessor class of a relationship. (Contributed by ML, 25-Oct-2020)

	Ref	Expression
Assertion	csbpredg	$$⊢A\in V\to ⦋A/x⦌Pred\left(R,D,X\right)=Pred\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌X\right)$$

Proof

Step	Hyp	Ref	Expression
1		csbin	$$⊢⦋A/x⦌\left(D\cap R^{-1}\left[\left\{X\right\}\right]\right)=⦋A/x⦌D\cap ⦋A/x⦌R^{-1}\left[\left\{X\right\}\right]$$
2		csbima12	$$⊢⦋A/x⦌R^{-1}\left[\left\{X\right\}\right]=⦋A/x⦌R^{-1}\left[⦋A/x⦌\left\{X\right\}\right]$$
3		csbcnv	$$⊢{⦋A/x⦌R}^{-1}=⦋A/x⦌R^{-1}$$
4	3	imaeq1i	$$⊢{⦋A/x⦌R}^{-1}\left[⦋A/x⦌\left\{X\right\}\right]=⦋A/x⦌R^{-1}\left[⦋A/x⦌\left\{X\right\}\right]$$
5		csbsng	$$⊢A\in V\to ⦋A/x⦌\left\{X\right\}=\left\{⦋A/x⦌X\right\}$$
6	5	imaeq2d	$$⊢A\in V\to {⦋A/x⦌R}^{-1}\left[⦋A/x⦌\left\{X\right\}\right]={⦋A/x⦌R}^{-1}\left[\left\{⦋A/x⦌X\right\}\right]$$
7	4 6	syl5eqr	$$⊢A\in V\to ⦋A/x⦌R^{-1}\left[⦋A/x⦌\left\{X\right\}\right]={⦋A/x⦌R}^{-1}\left[\left\{⦋A/x⦌X\right\}\right]$$
8	2 7	syl5eq	$$⊢A\in V\to ⦋A/x⦌R^{-1}\left[\left\{X\right\}\right]={⦋A/x⦌R}^{-1}\left[\left\{⦋A/x⦌X\right\}\right]$$
9	8	ineq2d	$$⊢A\in V\to ⦋A/x⦌D\cap ⦋A/x⦌R^{-1}\left[\left\{X\right\}\right]=⦋A/x⦌D\cap {⦋A/x⦌R}^{-1}\left[\left\{⦋A/x⦌X\right\}\right]$$
10	1 9	syl5eq	$$⊢A\in V\to ⦋A/x⦌\left(D\cap R^{-1}\left[\left\{X\right\}\right]\right)=⦋A/x⦌D\cap {⦋A/x⦌R}^{-1}\left[\left\{⦋A/x⦌X\right\}\right]$$
11		df-pred	$$⊢Pred\left(R,D,X\right)=D\cap R^{-1}\left[\left\{X\right\}\right]$$
12	11	csbeq2i	$$⊢⦋A/x⦌Pred\left(R,D,X\right)=⦋A/x⦌\left(D\cap R^{-1}\left[\left\{X\right\}\right]\right)$$
13		df-pred	$$⊢Pred\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌X\right)=⦋A/x⦌D\cap {⦋A/x⦌R}^{-1}\left[\left\{⦋A/x⦌X\right\}\right]$$
14	10 12 13	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌Pred\left(R,D,X\right)=Pred\left(⦋A/x⦌R,⦋A/x⦌D,⦋A/x⦌X\right)$$