Metamath Proof Explorer


Theorem nfof

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

Ref Expression
Hypothesis nfof.1
|- F/_ x R
Assertion nfof
|- F/_ x oF R

Proof

Step Hyp Ref Expression
1 nfof.1
 |-  F/_ x R
2 df-of
 |-  oF R = ( u e. _V , v e. _V |-> ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) ) )
3 nfcv
 |-  F/_ x _V
4 nfcv
 |-  F/_ x ( dom u i^i dom v )
5 nfcv
 |-  F/_ x ( u ` w )
6 nfcv
 |-  F/_ x ( v ` w )
7 5 1 6 nfov
 |-  F/_ x ( ( u ` w ) R ( v ` w ) )
8 4 7 nfmpt
 |-  F/_ x ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) )
9 3 3 8 nfmpo
 |-  F/_ x ( u e. _V , v e. _V |-> ( w e. ( dom u i^i dom v ) |-> ( ( u ` w ) R ( v ` w ) ) ) )
10 2 9 nfcxfr
 |-  F/_ x oF R