Metamath Proof Explorer


Theorem nfofr

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

Ref Expression
Hypothesis nfof.1 _ x R
Assertion nfofr _ x r R

Proof

Step Hyp Ref Expression
1 nfof.1 _ x R
2 df-ofr r R = u v | w dom u dom v u w R v w
3 nfcv _ x dom u dom v
4 nfcv _ x u w
5 nfcv _ x v w
6 4 1 5 nfbr x u w R v w
7 3 6 nfralw x w dom u dom v u w R v w
8 7 nfopab _ x u v | w dom u dom v u w R v w
9 2 8 nfcxfr _ x r R