Metamath Proof Explorer

Theorem rdgvalg

Description: Value of the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion rdgvalg ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ B = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F A ↾ B

Proof

Step Hyp Ref Expression
1 df-rdg ⊢ rec ⁡ F A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
2 1 tfr2a ⊢ B ∈ dom ⁡ rec ⁡ F A → rec ⁡ F A ⁡ B = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g ⁡ rec ⁡ F A ↾ B