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	|- F/_ x F
	nfrdg.2	|- F/_ x A
Assertion	nfrdg	|- F/_ x rec ( F , A )

Proof

Step	Hyp	Ref	Expression
1		nfrdg.1	|- F/_ x F
2		nfrdg.2	|- F/_ x A
3		df-rdg	|- rec ( F , A ) = recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
4		nfcv	|- F/_ x _V
5		nfv	|- F/ x g = (/)
6		nfv	|- F/ x Lim dom g
7		nfcv	|- F/_ x U. ran g
8		nfcv	|- F/_ x ( g ` U. dom g )
9	1 8	nffv	|- F/_ x ( F ` ( g ` U. dom g ) )
10	6 7 9	nfif	|- F/_ x if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) )
11	5 2 10	nfif	|- F/_ x if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) )
12	4 11	nfmpt	|- F/_ x ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) )
13	12	nfrecs	|- F/_ x recs ( ( g e. _V |-> if ( g = (/) , A , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )
14	3 13	nfcxfr	|- F/_ x rec ( F , A )