Theorem rdgsucmpt2

Description: This version of rdgsucmpt avoids the not-free hypothesis of rdgsucmptf by using two substitutions instead of one. (Contributed by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	rdgsucmpt2.1	|- F = rec ( ( x e. _V |-> C ) , A )
	rdgsucmpt2.2	|- ( y = x -> E = C )
	rdgsucmpt2.3	|- ( y = ( F ` B ) -> E = D )
Assertion	rdgsucmpt2	|- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )

Proof

Step	Hyp	Ref	Expression
1		rdgsucmpt2.1	|- F = rec ( ( x e. _V |-> C ) , A )
2		rdgsucmpt2.2	|- ( y = x -> E = C )
3		rdgsucmpt2.3	|- ( y = ( F ` B ) -> E = D )
4		nfcv	|- F/_ y A
5		nfcv	|- F/_ y B
6		nfcv	|- F/_ y D
7	2	cbvmptv	|- ( y e. _V |-> E ) = ( x e. _V |-> C )
8		rdgeq1	|- ( ( y e. _V |-> E ) = ( x e. _V |-> C ) -> rec ( ( y e. _V |-> E ) , A ) = rec ( ( x e. _V |-> C ) , A ) )
9	7 8	ax-mp	|- rec ( ( y e. _V |-> E ) , A ) = rec ( ( x e. _V |-> C ) , A )
10	1 9	eqtr4i	|- F = rec ( ( y e. _V |-> E ) , A )
11	4 5 6 10 3	rdgsucmptf	|- ( ( B e. On /\ D e. V ) -> ( F ` suc B ) = D )