Metamath Proof Explorer


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 𝐵 ) = 𝐷 )