Theorem rdglim2a

Description: The value of the recursive definition generator at a limit ordinal, in terms of indexed union of all smaller values. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	rdglim2a	|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U_ x e. B ( rec ( F , A ) ` x ) )

Proof

Step	Hyp	Ref	Expression
1		rdglim2	|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U. { y | E. x e. B y = ( rec ( F , A ) ` x ) } )
2		fvex	|- ( rec ( F , A ) ` x ) e. _V
3	2	dfiun2	|- U_ x e. B ( rec ( F , A ) ` x ) = U. { y | E. x e. B y = ( rec ( F , A ) ` x ) }
4	1 3	eqtr4di	|- ( ( B e. C /\ Lim B ) -> ( rec ( F , A ) ` B ) = U_ x e. B ( rec ( F , A ) ` x ) )