Metamath Proof Explorer

Theorem predeq123

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

Ref Expression
Assertion predeq123 
|- ( ( R = S /\ A = B /\ X = Y ) -> Pred ( R , A , X ) = Pred ( S , B , Y ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> A = B )
2 cnveq 
 |-  ( R = S -> `' R = `' S )
3 2 3ad2ant1 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> `' R = `' S )
4 sneq 
 |-  ( X = Y -> { X } = { Y } )
5 4 3ad2ant3 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> { X } = { Y } )
6 3 5 imaeq12d 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> ( `' R " { X } ) = ( `' S " { Y } ) )
7 1 6 ineq12d 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> ( A i^i ( `' R " { X } ) ) = ( B i^i ( `' S " { Y } ) ) )
8 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
9 df-pred 
 |-  Pred ( S , B , Y ) = ( B i^i ( `' S " { Y } ) )
10 7 8 9 3eqtr4g 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> Pred ( R , A , X ) = Pred ( S , B , Y ) )