Theorem rdgsucmpt

Description: The value of the recursive definition generator at a successor (special case where the characteristic function uses the map operation). (Contributed by Mario Carneiro, 9-Sep-2013)

	Ref	Expression
Hypotheses	rdgsucmpt.1	⊢ 𝐹 = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
	rdgsucmpt.2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 )
Assertion	rdgsucmpt	⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		rdgsucmpt.1	⊢ 𝐹 = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
2		rdgsucmpt.2	⊢ ( 𝑥 = ( 𝐹 ‘ 𝐵 ) → 𝐶 = 𝐷 )
3		nfcv	⊢ Ⅎ 𝑥 𝐴
4		nfcv	⊢ Ⅎ 𝑥 𝐵
5		nfcv	⊢ Ⅎ 𝑥 𝐷
6	3 4 5 1 2	rdgsucmptf	⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )