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=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼C\right),A\right)$$
	rdgsucmpt.2	$$⊢x=F\left(B\right)\to C=D$$
Assertion	rdgsucmpt	$$⊢\left(B\in \mathrm{On}\wedge D\in V\right)\to F\left(\mathrm{suc}B\right)=D$$

Proof

Step	Hyp	Ref	Expression
1		rdgsucmpt.1	$$⊢F=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼C\right),A\right)$$
2		rdgsucmpt.2	$$⊢x=F\left(B\right)\to C=D$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
6	3 4 5 1 2	rdgsucmptf	$$⊢\left(B\in \mathrm{On}\wedge D\in V\right)\to F\left(\mathrm{suc}B\right)=D$$