Theorem nffvmpt1

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

	Ref	Expression
Assertion	nffvmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)$$
2		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
3	1 2	nffv	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼B\right)\left(C\right)$$