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	⊢ Ⅎ 𝑥 𝐹
	nffv.2	⊢ Ⅎ 𝑥 𝐴
Assertion	nffv	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nffv.1	⊢ Ⅎ 𝑥 𝐹
2		nffv.2	⊢ Ⅎ 𝑥 𝐴
3		df-fv	⊢ ( 𝐹 ‘ 𝐴 ) = ( ℩ 𝑦 𝐴 𝐹 𝑦 )
4		nfcv	⊢ Ⅎ 𝑥 𝑦
5	2 1 4	nfbr	⊢ Ⅎ 𝑥 𝐴 𝐹 𝑦
6	5	nfiotaw	⊢ Ⅎ 𝑥 ( ℩ 𝑦 𝐴 𝐹 𝑦 )
7	3 6	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 )