Theorem fr0g

Description: The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996)

	Ref	Expression
Assertion	fr0g	|- ( A e. B -> ( ( rec ( F , A ) |` _om ) ` (/) ) = A )

Proof

Step	Hyp	Ref	Expression
1		peano1	|- (/) e. _om
2		fvres	|- ( (/) e. _om -> ( ( rec ( F , A ) |` _om ) ` (/) ) = ( rec ( F , A ) ` (/) ) )
3	1 2	ax-mp	|- ( ( rec ( F , A ) |` _om ) ` (/) ) = ( rec ( F , A ) ` (/) )
4		rdg0g	|- ( A e. B -> ( rec ( F , A ) ` (/) ) = A )
5	3 4	eqtrid	|- ( A e. B -> ( ( rec ( F , A ) |` _om ) ` (/) ) = A )