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 F = rec x V C A
rdgsucmpt.2 x = F B C = D
Assertion rdgsucmpt B On D V F suc B = D

Proof

Step Hyp Ref Expression
1 rdgsucmpt.1 F = rec x V C A
2 rdgsucmpt.2 x = F B C = D
3 nfcv _ x A
4 nfcv _ x B
5 nfcv _ x D
6 3 4 5 1 2 rdgsucmptf B On D V F suc B = D