Theorem nfof

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

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

Proof

Step	Hyp	Ref	Expression
1		nfof.1	|- F/_ x R
2		df-of	|- oF R = ( u e. _V , v e. _V |-> ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) ) )
3		nfcv	|- F/_ x _V
4		nfcv	|- F/_ x ( dom u i^i dom v )
5		nfcv	|- F/_ x ( u ` w )
6		nfcv	|- F/_ x ( v ` w )
7	5 1 6	nfov	|- F/_ x ( ( u ` w ) R ( v ` w ) )
8	4 7	nfmpt	|- F/_ x ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) )
9	3 3 8	nfmpo	|- F/_ x ( u e. _V , v e. _V |-> ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) ) )
10	2 9	nfcxfr	|- F/_ x oF R