Theorem nfof

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

	Ref	Expression
Hypothesis	nfof.1	⊢ Ⅎ 𝑥 𝑅
Assertion	nfof	⊢ Ⅎ 𝑥 ∘f 𝑅

Proof

Step	Hyp	Ref	Expression
1		nfof.1	⊢ Ⅎ 𝑥 𝑅
2		df-of	⊢ ∘f 𝑅 = ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ↦ ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) ) ) )
3		nfcv	⊢ Ⅎ 𝑥 V
4		nfcv	⊢ Ⅎ 𝑥 ( dom 𝑢 ∩ dom 𝑣 )
5		nfcv	⊢ Ⅎ 𝑥 ( 𝑢 ‘ 𝑤 )
6		nfcv	⊢ Ⅎ 𝑥 ( 𝑣 ‘ 𝑤 )
7	5 1 6	nfov	⊢ Ⅎ 𝑥 ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) )
8	4 7	nfmpt	⊢ Ⅎ 𝑥 ( 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ↦ ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) ) )
9	3 3 8	nfmpo	⊢ Ⅎ 𝑥 ( 𝑢 ∈ V , 𝑣 ∈ V ↦ ( 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ↦ ( ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) ) ) )
10	2 9	nfcxfr	⊢ Ⅎ 𝑥 ∘f 𝑅