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 )