Theorem nfofr

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

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

Proof

Step	Hyp	Ref	Expression
1		nfof.1	⊢ Ⅎ 𝑥 𝑅
2		df-ofr	⊢ ∘r 𝑅 = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∀ 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) }
3		nfcv	⊢ Ⅎ 𝑥 ( dom 𝑢 ∩ dom 𝑣 )
4		nfcv	⊢ Ⅎ 𝑥 ( 𝑢 ‘ 𝑤 )
5		nfcv	⊢ Ⅎ 𝑥 ( 𝑣 ‘ 𝑤 )
6	4 1 5	nfbr	⊢ Ⅎ 𝑥 ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 )
7	3 6	nfralw	⊢ Ⅎ 𝑥 ∀ 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 )
8	7	nfopab	⊢ Ⅎ 𝑥 { ⟨ 𝑢 , 𝑣 ⟩ ∣ ∀ 𝑤 ∈ ( dom 𝑢 ∩ dom 𝑣 ) ( 𝑢 ‘ 𝑤 ) 𝑅 ( 𝑣 ‘ 𝑤 ) }
9	2 8	nfcxfr	⊢ Ⅎ 𝑥 ∘r 𝑅