Metamath Proof Explorer


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 𝑅