Metamath Proof Explorer


Theorem wrecseq1

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

Ref Expression
Assertion wrecseq1
|- ( R = S -> wrecs ( R , A , F ) = wrecs ( S , A , F ) )

Proof

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