Theorem recsval

Description: Strong transfinite recursion in terms of all previous values. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Assertion	recsval	$$⊢A\in \mathrm{On}\to \mathrm{recs}\left(F\right)\left(A\right)=F\left({\mathrm{recs}\left(F\right)\upharpoonright }_A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\mathrm{recs}\left(F\right)=\mathrm{recs}\left(F\right)$$
2	1	tfr2	$$⊢A\in \mathrm{On}\to \mathrm{recs}\left(F\right)\left(A\right)=F\left({\mathrm{recs}\left(F\right)\upharpoonright }_A\right)$$