Metamath Proof Explorer

Theorem csbpredg

Description: Move class substitution in and out of the predecessor class of a relation. (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 eqtrid 
 |-  ( 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 eqtrid 
 |-  ( 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 ) )