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	⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
	frsucmpt2w.2	⊢ ( 𝑦 = 𝑥 → 𝐸 = 𝐶 )
	frsucmpt2w.3	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → 𝐸 = 𝐷 )
Assertion	frsucmpt2w	⊢ ( ( 𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		frsucmpt2w.1	⊢ 𝐹 = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
2		frsucmpt2w.2	⊢ ( 𝑦 = 𝑥 → 𝐸 = 𝐶 )
3		frsucmpt2w.3	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) → 𝐸 = 𝐷 )
4		nfcv	⊢ Ⅎ 𝑦 𝐴
5		nfcv	⊢ Ⅎ 𝑦 𝐵
6		nfcv	⊢ Ⅎ 𝑦 𝐷
7	2	cbvmptv	⊢ ( 𝑦 ∈ V ↦ 𝐸 ) = ( 𝑥 ∈ V ↦ 𝐶 )
8		rdgeq1	⊢ ( ( 𝑦 ∈ V ↦ 𝐸 ) = ( 𝑥 ∈ V ↦ 𝐶 ) → rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) )
9	7 8	ax-mp	⊢ rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) = rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 )
10	9	reseq1i	⊢ ( rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ 𝐶 ) , 𝐴 ) ↾ ω )
11	1 10	eqtr4i	⊢ 𝐹 = ( rec ( ( 𝑦 ∈ V ↦ 𝐸 ) , 𝐴 ) ↾ ω )
12	4 5 6 11 3	frsucmpt	⊢ ( ( 𝐵 ∈ ω ∧ 𝐷 ∈ 𝑉 ) → ( 𝐹 ‘ suc 𝐵 ) = 𝐷 )