Theorem nffv

Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 14-Nov-1995) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nffv.1	$$⊢\underset{\_}{Ⅎ}xF$$
	nffv.2	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nffv.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		nffv.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		df-fv	$$⊢F\left(A\right)=\left(\iota y|AFy\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
5	2 1 4	nfbr	$$⊢ℲxAFy$$
6	5	nfiotaw	$$⊢\underset{\_}{Ⅎ}x\left(\iota y|AFy\right)$$
7	3 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}xF\left(A\right)$$