Theorem nfofr

Description: Hypothesis builder for function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypothesis	nfof.1	|- F/_ x R
Assertion	nfofr	|- F/_ x oR R

Proof

Step	Hyp	Ref	Expression
1		nfof.1	|- F/_ x R
2		df-ofr	|- oR R = { <. u , v >. | A. w e. ( dom u i^i dom v ) ( u ` w ) R ( v ` w ) }
3		nfcv	|- F/_ x ( dom u i^i dom v )
4		nfcv	|- F/_ x ( u ` w )
5		nfcv	|- F/_ x ( v ` w )
6	4 1 5	nfbr	|- F/ x ( u ` w ) R ( v ` w )
7	3 6	nfralw	|- F/ x A. w e. ( dom u i^i dom v ) ( u ` w ) R ( v ` w )
8	7	nfopab	|- F/_ x { <. u , v >. | A. w e. ( dom u i^i dom v ) ( u ` w ) R ( v ` w ) }
9	2 8	nfcxfr	|- F/_ x oR R