Metamath Proof Explorer

Theorem wrecseq3

Description: Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018)

Ref Expression
Assertion wrecseq3 
|- ( F = G -> wrecs ( R , A , F ) = wrecs ( R , A , G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  R = R
2 eqid 
 |-  A = A
3 wrecseq123 
 |-  ( ( R = R /\ A = A /\ F = G ) -> wrecs ( R , A , F ) = wrecs ( R , A , G ) )
4 1 2 3 mp3an12 
 |-  ( F = G -> wrecs ( R , A , F ) = wrecs ( R , A , G ) )