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 ) |