Theorem nffvmpt1

Description: Bound-variable hypothesis builder for mapping, special case. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Assertion	nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		nfcv	⊢ Ⅎ 𝑥 𝐶
3	1 2	nffv	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐶 )