Theorem nfrdg

Description: Bound-variable hypothesis builder for the recursive definition generator. (Contributed by NM, 14-Sep-2003) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Hypotheses	nfrdg.1	⊢ Ⅎ 𝑥 𝐹
	nfrdg.2	⊢ Ⅎ 𝑥 𝐴
Assertion	nfrdg	⊢ Ⅎ 𝑥 rec ( 𝐹 , 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfrdg.1	⊢ Ⅎ 𝑥 𝐹
2		nfrdg.2	⊢ Ⅎ 𝑥 𝐴
3		df-rdg	⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
4		nfcv	⊢ Ⅎ 𝑥 V
5		nfv	⊢ Ⅎ 𝑥 𝑔 = ∅
6		nfv	⊢ Ⅎ 𝑥 Lim dom 𝑔
7		nfcv	⊢ Ⅎ 𝑥 ∪ ran 𝑔
8		nfcv	⊢ Ⅎ 𝑥 ( 𝑔 ‘ ∪ dom 𝑔 )
9	1 8	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) )
10	6 7 9	nfif	⊢ Ⅎ 𝑥 if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) )
11	5 2 10	nfif	⊢ Ⅎ 𝑥 if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) )
12	4 11	nfmpt	⊢ Ⅎ 𝑥 ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) )
13	12	nfrecs	⊢ Ⅎ 𝑥 recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
14	3 13	nfcxfr	⊢ Ⅎ 𝑥 rec ( 𝐹 , 𝐴 )