Metamath Proof Explorer


Theorem nfafv

Description: Bound-variable hypothesis builder for function value, analogous to nffv . To prove a deduction version of this analogous to nffvd is not easily possible because a deduction version of nfdfat cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Hypotheses nfafv.1
|- F/_ x F
nfafv.2
|- F/_ x A
Assertion nfafv
|- F/_ x ( F ''' A )

Proof

Step Hyp Ref Expression
1 nfafv.1
 |-  F/_ x F
2 nfafv.2
 |-  F/_ x A
3 dfafv2
 |-  ( F ''' A ) = if ( F defAt A , ( F ` A ) , _V )
4 1 2 nfdfat
 |-  F/ x F defAt A
5 1 2 nffv
 |-  F/_ x ( F ` A )
6 nfcv
 |-  F/_ x _V
7 4 5 6 nfif
 |-  F/_ x if ( F defAt A , ( F ` A ) , _V )
8 3 7 nfcxfr
 |-  F/_ x ( F ''' A )