Metamath Proof Explorer


Theorem nfof

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

Ref Expression
Hypothesis nfof.1 _ x R
Assertion nfof _ x f R

Proof

Step Hyp Ref Expression
1 nfof.1 _ x R
2 df-of f R = u V , v V w dom u dom v u w R v w
3 nfcv _ x V
4 nfcv _ x dom u dom v
5 nfcv _ x u w
6 nfcv _ x v w
7 5 1 6 nfov _ x u w R v w
8 4 7 nfmpt _ x w dom u dom v u w R v w
9 3 3 8 nfmpo _ x u V , v V w dom u dom v u w R v w
10 2 9 nfcxfr _ x f R