Metamath Proof Explorer

Theorem rdgeq2

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

Ref Expression
Assertion rdgeq2 
|- ( A = B -> rec ( F , A ) = rec ( F , B ) )

Proof

Step Hyp Ref Expression
1 ifeq1 
 |-  ( A = B -> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) = if ( g = (/) , B , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) )
2 1 mpteq2dv 
 |-  ( A = B -> ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , B , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
3 recseq 
 |-  ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) = ( g e. _V |-> if ( g = (/) , B , 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 , ( F ` ( g ` U. dom g ) ) ) ) ) ) = recs ( ( g e. _V |-> if ( g = (/) , B , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) )
4 2 3 syl 
 |-  ( A = B -> 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 = (/) , B , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) )
5 df-rdg 
 |-  rec ( F , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
6 df-rdg 
 |-  rec ( F , B ) = recs ( ( g e. _V |-> if ( g = (/) , B , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
7 4 5 6 3eqtr4g 
 |-  ( A = B -> rec ( F , A ) = rec ( F , B ) )