Metamath Proof Explorer

Theorem fr0g

Description: The initial value resulting from finite recursive definition generation. (Contributed by NM, 15-Oct-1996)

Ref Expression
Assertion fr0g ⊢ A ∈ B → rec ⁡ F A ↾ ω ⁡ ∅ = A

Proof

Step Hyp Ref Expression
1 peano1 ⊢ ∅ ∈ ω
2 fvres ⊢ ∅ ∈ ω → rec ⁡ F A ↾ ω ⁡ ∅ = rec ⁡ F A ⁡ ∅
3 1 2 ax-mp ⊢ rec ⁡ F A ↾ ω ⁡ ∅ = rec ⁡ F A ⁡ ∅
4 rdg0g ⊢ A ∈ B → rec ⁡ F A ⁡ ∅ = A
5 3 4 syl5eq ⊢ A ∈ B → rec ⁡ F A ↾ ω ⁡ ∅ = A