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 ∈ V ⟼ C A ↾ ω
frsucmpt2w.2 ⊢ y = x → E = C
frsucmpt2w.3 ⊢ y = F ⁡ B → E = D
Assertion frsucmpt2w ⊢ B ∈ ω ∧ D ∈ V → F ⁡ suc ⁡ B = D

Proof

Step Hyp Ref Expression
1 frsucmpt2w.1 ⊢ F = rec ⁡ x ∈ V ⟼ C A ↾ ω
2 frsucmpt2w.2 ⊢ y = x → E = C
3 frsucmpt2w.3 ⊢ y = F ⁡ B → E = D
4 nfcv ⊢ Ⅎ _ y A
5 nfcv ⊢ Ⅎ _ y B
6 nfcv ⊢ Ⅎ _ y D
7 2 cbvmptv ⊢ y ∈ V ⟼ E = x ∈ V ⟼ C
8 rdgeq1 ⊢ y ∈ V ⟼ E = x ∈ V ⟼ C → rec ⁡ y ∈ V ⟼ E A = rec ⁡ x ∈ V ⟼ C A
9 7 8 ax-mp ⊢ rec ⁡ y ∈ V ⟼ E A = rec ⁡ x ∈ V ⟼ C A
10 9 reseq1i ⊢ rec ⁡ y ∈ V ⟼ E A ↾ ω = rec ⁡ x ∈ V ⟼ C A ↾ ω
11 1 10 eqtr4i ⊢ F = rec ⁡ y ∈ V ⟼ E A ↾ ω
12 4 5 6 11 3 frsucmpt ⊢ B ∈ ω ∧ D ∈ V → F ⁡ suc ⁡ B = D