Description: Boundvariable hypothesis builder for a function with domain. (Contributed by NM, 30Jan2004)
Ref  Expression  

Hypotheses  nffn.1   F/_ x F 

nffn.2   F/_ x A 

Assertion  nffn   F/ x F Fn A 
Step  Hyp  Ref  Expression 

1  nffn.1   F/_ x F 

2  nffn.2   F/_ x A 

3  dffn   ( F Fn A <> ( Fun F /\ dom F = A ) ) 

4  1  nffun   F/ x Fun F 
5  1  nfdm   F/_ x dom F 
6  5 2  nfeq   F/ x dom F = A 
7  4 6  nfan   F/ x ( Fun F /\ dom F = A ) 
8  3 7  nfxfr   F/ x F Fn A 