Theorem mptfng

Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011)

	Ref	Expression
Hypothesis	mptfng.1	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	mptfng	$$⊢\forall x\in AB\in \mathrm{V}\leftrightarrow FFnA$$

Proof

Step	Hyp	Ref	Expression
1		mptfng.1	$$⊢F=\left(x\in A⟼B\right)$$
2		eueq	$$⊢B\in \mathrm{V}\leftrightarrow \exists !yy=B$$
3	2	ralbii	$$⊢\forall x\in AB\in \mathrm{V}\leftrightarrow \forall x\in A\exists !yy=B$$
4		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
5	1 4	eqtri	$$⊢F=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
6	5	fnopabg	$$⊢\forall x\in A\exists !yy=B\leftrightarrow FFnA$$
7	3 6	bitri	$$⊢\forall x\in AB\in \mathrm{V}\leftrightarrow FFnA$$