Theorem predeq123

Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018)

	Ref	Expression
Assertion	predeq123	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to Pred\left(R,A,X\right)=Pred\left(S,B,Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp2	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to A=B$$
2		cnveq	$$⊢R=S\to R^{-1}=S^{-1}$$
3	2	3ad2ant1	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to R^{-1}=S^{-1}$$
4		sneq	$$⊢X=Y\to \left\{X\right\}=\left\{Y\right\}$$
5	4	3ad2ant3	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to \left\{X\right\}=\left\{Y\right\}$$
6	3 5	imaeq12d	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to R^{-1}\left[\left\{X\right\}\right]=S^{-1}\left[\left\{Y\right\}\right]$$
7	1 6	ineq12d	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to A\cap R^{-1}\left[\left\{X\right\}\right]=B\cap S^{-1}\left[\left\{Y\right\}\right]$$
8		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
9		df-pred	$$⊢Pred\left(S,B,Y\right)=B\cap S^{-1}\left[\left\{Y\right\}\right]$$
10	7 8 9	3eqtr4g	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to Pred\left(R,A,X\right)=Pred\left(S,B,Y\right)$$