Metamath Proof Explorer

Theorem rdg0g

Description: The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995)

Ref Expression
Assertion rdg0g 
|- ( A e. C -> ( rec ( F , A ) ` (/) ) = A )

Proof

Step Hyp Ref Expression
1 rdgeq2 
 |-  ( x = A -> rec ( F , x ) = rec ( F , A ) )
2 1 fveq1d 
 |-  ( x = A -> ( rec ( F , x ) ` (/) ) = ( rec ( F , A ) ` (/) ) )
3 id 
 |-  ( x = A -> x = A )
4 2 3 eqeq12d 
 |-  ( x = A -> ( ( rec ( F , x ) ` (/) ) = x <-> ( rec ( F , A ) ` (/) ) = A ) )
5 vex 
 |-  x e. _V
6 5 rdg0 
 |-  ( rec ( F , x ) ` (/) ) = x
7 4 6 vtoclg 
 |-  ( A e. C -> ( rec ( F , A ) ` (/) ) = A )