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 e. V -> [_ A / x ]_ Pred ( R , D , X ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ X ) )

Proof

Step	Hyp	Ref	Expression
1		csbin	|- [_ A / x ]_ ( D i^i ( `' R " { X } ) ) = ( [_ A / x ]_ D i^i [_ A / x ]_ ( `' R " { X } ) )
2		csbima12	|- [_ A / x ]_ ( `' R " { X } ) = ( [_ A / x ]_ `' R " [_ A / x ]_ { X } )
3		csbcnv	|- `' [_ A / x ]_ R = [_ A / x ]_ `' R
4	3	imaeq1i	|- ( `' [_ A / x ]_ R " [_ A / x ]_ { X } ) = ( [_ A / x ]_ `' R " [_ A / x ]_ { X } )
5		csbsng	|- ( A e. V -> [_ A / x ]_ { X } = { [_ A / x ]_ X } )
6	5	imaeq2d	|- ( A e. V -> ( `' [_ A / x ]_ R " [_ A / x ]_ { X } ) = ( `' [_ A / x ]_ R " { [_ A / x ]_ X } ) )
7	4 6	eqtr3id	|- ( A e. V -> ( [_ A / x ]_ `' R " [_ A / x ]_ { X } ) = ( `' [_ A / x ]_ R " { [_ A / x ]_ X } ) )
8	2 7	syl5eq	|- ( A e. V -> [_ A / x ]_ ( `' R " { X } ) = ( `' [_ A / x ]_ R " { [_ A / x ]_ X } ) )
9	8	ineq2d	|- ( A e. V -> ( [_ A / x ]_ D i^i [_ A / x ]_ ( `' R " { X } ) ) = ( [_ A / x ]_ D i^i ( `' [_ A / x ]_ R " { [_ A / x ]_ X } ) ) )
10	1 9	syl5eq	|- ( A e. V -> [_ A / x ]_ ( D i^i ( `' R " { X } ) ) = ( [_ A / x ]_ D i^i ( `' [_ A / x ]_ R " { [_ A / x ]_ X } ) ) )
11		df-pred	|- Pred ( R , D , X ) = ( D i^i ( `' R " { X } ) )
12	11	csbeq2i	|- [_ A / x ]_ Pred ( R , D , X ) = [_ A / x ]_ ( D i^i ( `' R " { X } ) )
13		df-pred	|- Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ X ) = ( [_ A / x ]_ D i^i ( `' [_ A / x ]_ R " { [_ A / x ]_ X } ) )
14	10 12 13	3eqtr4g	|- ( A e. V -> [_ A / x ]_ Pred ( R , D , X ) = Pred ( [_ A / x ]_ R , [_ A / x ]_ D , [_ A / x ]_ X ) )