This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )