Metamath Proof Explorer


Theorem frsucmpt2w

Description: Version of frsucmpt2 with a disjoint variable condition, which does not require ax-13 . (Contributed by Gino Giotto, 26-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 frsucmpt2w.1
 |-  F = ( rec ( ( x e. _V |-> C ) , A ) |` _om )
2 frsucmpt2w.2
 |-  ( y = x -> E = C )
3 frsucmpt2w.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 9 reseq1i
 |-  ( rec ( ( y e. _V |-> E ) , A ) |` _om ) = ( rec ( ( x e. _V |-> C ) , A ) |` _om )
11 1 10 eqtr4i
 |-  F = ( rec ( ( y e. _V |-> E ) , A ) |` _om )
12 4 5 6 11 3 frsucmpt
 |-  ( ( B e. _om /\ D e. V ) -> ( F ` suc B ) = D )