Metamath Proof Explorer

Theorem wsuceq123

Description: Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> R = S )
2 1 cnveqd 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> `' R = `' S )
3 predeq123 
 |-  ( ( `' R = `' S /\ A = B /\ X = Y ) -> Pred ( `' R , A , X ) = Pred ( `' S , B , Y ) )
4 2 3 syld3an1 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> Pred ( `' R , A , X ) = Pred ( `' S , B , Y ) )
5 simp2 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> A = B )
6 4 5 1 infeq123d 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> inf ( Pred ( `' R , A , X ) , A , R ) = inf ( Pred ( `' S , B , Y ) , B , S ) )
7 df-wsuc 
 |-  wsuc ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )
8 df-wsuc 
 |-  wsuc ( S , B , Y ) = inf ( Pred ( `' S , B , Y ) , B , S )
9 6 7 8 3eqtr4g 
 |-  ( ( R = S /\ A = B /\ X = Y ) -> wsuc ( R , A , X ) = wsuc ( S , B , Y ) )