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⁡FA→rec⁡FA⁡B=g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡rec⁡FA↾B

Proof

Step Hyp Ref Expression
1 df-rdg ⊢rec⁡FA=recs⁡g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g
2 1 tfr2a ⊢B∈dom⁡rec⁡FA→rec⁡FA⁡B=g∈V⟼ifg=∅AifLim⁡dom⁡g⋃ran⁡gF⁡g⁡⋃dom⁡g⁡rec⁡FA↾B