Theorem recsval

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

	Ref	Expression
Assertion	recsval	⊢ ( 𝐴 ∈ On → ( recs ( 𝐹 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ recs ( 𝐹 ) = recs ( 𝐹 )
2	1	tfr2	⊢ ( 𝐴 ∈ On → ( recs ( 𝐹 ) ‘ 𝐴 ) = ( 𝐹 ‘ ( recs ( 𝐹 ) ↾ 𝐴 ) ) )