Metamath Proof Explorer

Theorem rdgeq1

Description: Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion rdgeq1 
|- ( F = G -> rec ( F , A ) = rec ( G , A ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( F = G -> ( F ` ( g ` U. dom g ) ) = ( G ` ( g ` U. dom g ) ) )
2 1 ifeq2d 
 |-  ( F = G -> if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) = if ( Lim dom g , U. ran g , ( G ` ( g ` U. dom g ) ) ) )
3 2 ifeq2d 
 |-  ( F = G -> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = if ( g = (/) , A , if ( Lim dom g , U. ran g , ( G ` ( g ` U. dom g ) ) ) ) )
4 3 mpteq2dv 
 |-  ( F = G -> ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( G ` ( g ` U. dom g ) ) ) ) ) )
5 recseq 
 |-  ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( G ` ( g ` U. dom g ) ) ) ) ) -> recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( G ` ( g ` U. dom g ) ) ) ) ) ) )
6 4 5 syl 
 |-  ( F = G -> recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( G ` ( g ` U. dom g ) ) ) ) ) ) )
7 df-rdg 
 |-  rec ( F , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
8 df-rdg 
 |-  rec ( G , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( G ` ( g ` U. dom g ) ) ) ) ) )
9 6 7 8 3eqtr4g 
 |-  ( F = G -> rec ( F , A ) = rec ( G , A ) )