Theorem mptfnd

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013) (Revised by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	mptfnd.1	$$⊢\underset{\_}{Ⅎ}xA$$
	mptfnd.2	$$⊢Ⅎx\phi$$
	mptfnd.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
Assertion	mptfnd	$$⊢\phi \to \left(x\in A⟼B\right)FnA$$

Proof

Step	Hyp	Ref	Expression
1		mptfnd.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		mptfnd.2	$$⊢Ⅎx\phi$$
3		mptfnd.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
4	3	ex	$$⊢\phi \to \left(x\in A\to B\in V\right)$$
5		elex	$$⊢B\in V\to B\in \mathrm{V}$$
6	4 5	syl6	$$⊢\phi \to \left(x\in A\to B\in \mathrm{V}\right)$$
7	2 6	ralrimi	$$⊢\phi \to \forall x\in AB\in \mathrm{V}$$
8	1	mptfnf	$$⊢\forall x\in AB\in \mathrm{V}\leftrightarrow \left(x\in A⟼B\right)FnA$$
9	7 8	sylib	$$⊢\phi \to \left(x\in A⟼B\right)FnA$$