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 𝐹 = ( 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 𝐵 ) = 𝐷 )