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 ) )