Metamath Proof Explorer


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 𝑅