Theorem dffn5f

Description: Representation of a function in terms of its values. (Contributed by Mario Carneiro, 3-Jul-2015)

	Ref	Expression
Hypothesis	dffn5f.1	$$⊢\underset{\_}{Ⅎ}xF$$
Assertion	dffn5f	$$⊢FFnA\leftrightarrow F=\left(x\in A⟼F\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dffn5f.1	$$⊢\underset{\_}{Ⅎ}xF$$
2		dffn5	$$⊢FFnA\leftrightarrow F=\left(z\in A⟼F\left(z\right)\right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}xz$$
4	1 3	nffv	$$⊢\underset{\_}{Ⅎ}xF\left(z\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}zF\left(x\right)$$
6		fveq2	$$⊢z=x\to F\left(z\right)=F\left(x\right)$$
7	4 5 6	cbvmpt	$$⊢\left(z\in A⟼F\left(z\right)\right)=\left(x\in A⟼F\left(x\right)\right)$$
8	7	eqeq2i	$$⊢F=\left(z\in A⟼F\left(z\right)\right)\leftrightarrow F=\left(x\in A⟼F\left(x\right)\right)$$
9	2 8	bitri	$$⊢FFnA\leftrightarrow F=\left(x\in A⟼F\left(x\right)\right)$$