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	$$⊢\underset{\_}{Ⅎ}xF$$
	nfafv.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfafv	$$⊢\underset{\_}{Ⅎ}x\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfafv.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nfafv.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		dfafv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)$$
4	1 2	nfdfat	$$⊢ℲxF\mathrm{defAt}A$$
5	1 2	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(A\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}x\mathrm{V}$$
7	4 5 6	nfif	$$⊢\underset{\_}{Ⅎ}xif\left(F\mathrm{defAt}A,F\left(A\right),\mathrm{V}\right)$$
8	3 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}x\left(F\mathrm{\text{'}\text{'}\text{'}}A\right)$$