Theorem feqmptdf

Description: Deduction form of dffn5f . (Contributed by Mario Carneiro, 8-Jan-2015) (Revised by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	feqmptdf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	feqmptdf.2	$$⊢\underset{\_}{Ⅎ}xF$$
	feqmptdf.3	$$⊢\phi \to F:A⟶B$$
Assertion	feqmptdf	$$⊢\phi \to F=\left(x\in A⟼F\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		feqmptdf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		feqmptdf.2	$$⊢\underset{\_}{Ⅎ}xF$$
3		feqmptdf.3	$$⊢\phi \to F:A⟶B$$
4		ffn	$$⊢F:A⟶B\to FFnA$$
5		fnrel	$$⊢FFnA\to \mathrm{Rel}F$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}yF$$
7	2 6	dfrel4	$$⊢\mathrm{Rel}F\leftrightarrow F=\left\{⟨x,y⟩|xFy\right\}$$
8	5 7	sylib	$$⊢FFnA\to F=\left\{⟨x,y⟩|xFy\right\}$$
9	2 1	nffn	$$⊢ℲxFFnA$$
10		nfv	$$⊢ℲyFFnA$$
11		fnbr	$$⊢\left(FFnA\wedge xFy\right)\to x\in A$$
12	11	ex	$$⊢FFnA\to \left(xFy\to x\in A\right)$$
13	12	pm4.71rd	$$⊢FFnA\to \left(xFy\leftrightarrow \left(x\in A\wedge xFy\right)\right)$$
14		eqcom	$$⊢y=F\left(x\right)\leftrightarrow F\left(x\right)=y$$
15		fnbrfvb	$$⊢\left(FFnA\wedge x\in A\right)\to \left(F\left(x\right)=y\leftrightarrow xFy\right)$$
16	14 15	bitrid	$$⊢\left(FFnA\wedge x\in A\right)\to \left(y=F\left(x\right)\leftrightarrow xFy\right)$$
17	16	pm5.32da	$$⊢FFnA\to \left(\left(x\in A\wedge y=F\left(x\right)\right)\leftrightarrow \left(x\in A\wedge xFy\right)\right)$$
18	13 17	bitr4d	$$⊢FFnA\to \left(xFy\leftrightarrow \left(x\in A\wedge y=F\left(x\right)\right)\right)$$
19	9 10 18	opabbid	$$⊢FFnA\to \left\{⟨x,y⟩|xFy\right\}=\left\{⟨x,y⟩|\left(x\in A\wedge y=F\left(x\right)\right)\right\}$$
20	8 19	eqtrd	$$⊢FFnA\to F=\left\{⟨x,y⟩|\left(x\in A\wedge y=F\left(x\right)\right)\right\}$$
21		df-mpt	$$⊢\left(x\in A⟼F\left(x\right)\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=F\left(x\right)\right)\right\}$$
22	20 21	eqtr4di	$$⊢FFnA\to F=\left(x\in A⟼F\left(x\right)\right)$$
23	3 4 22	3syl	$$⊢\phi \to F=\left(x\in A⟼F\left(x\right)\right)$$