This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )