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 )