Theorem fgraphxp

Description: Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	fgraphxp	$$⊢F:A⟶B\to F=\left\{x\in \left(A\times B\right)|F\left(1^{st}\left(x\right)\right)=2^{nd}\left(x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fgraphopab	$$⊢F:A⟶B\to F=\left\{⟨a,b⟩|\left(\left(a\in A\wedge b\in B\right)\wedge F\left(a\right)=b\right)\right\}$$
2		vex	$$⊢a\in \mathrm{V}$$
3		vex	$$⊢b\in \mathrm{V}$$
4	2 3	op1std	$$⊢x=⟨a,b⟩\to 1^{st}\left(x\right)=a$$
5	4	fveq2d	$$⊢x=⟨a,b⟩\to F\left(1^{st}\left(x\right)\right)=F\left(a\right)$$
6	2 3	op2ndd	$$⊢x=⟨a,b⟩\to 2^{nd}\left(x\right)=b$$
7	5 6	eqeq12d	$$⊢x=⟨a,b⟩\to \left(F\left(1^{st}\left(x\right)\right)=2^{nd}\left(x\right)\leftrightarrow F\left(a\right)=b\right)$$
8	7	rabxp	$$⊢\left\{x\in \left(A\times B\right)|F\left(1^{st}\left(x\right)\right)=2^{nd}\left(x\right)\right\}=\left\{⟨a,b⟩|\left(a\in A\wedge b\in B\wedge F\left(a\right)=b\right)\right\}$$
9		df-3an	$$⊢\left(a\in A\wedge b\in B\wedge F\left(a\right)=b\right)\leftrightarrow \left(\left(a\in A\wedge b\in B\right)\wedge F\left(a\right)=b\right)$$
10	9	opabbii	$$⊢\left\{⟨a,b⟩|\left(a\in A\wedge b\in B\wedge F\left(a\right)=b\right)\right\}=\left\{⟨a,b⟩|\left(\left(a\in A\wedge b\in B\right)\wedge F\left(a\right)=b\right)\right\}$$
11	8 10	eqtri	$$⊢\left\{x\in \left(A\times B\right)|F\left(1^{st}\left(x\right)\right)=2^{nd}\left(x\right)\right\}=\left\{⟨a,b⟩|\left(\left(a\in A\wedge b\in B\right)\wedge F\left(a\right)=b\right)\right\}$$
12	1 11	syl6eqr	$$⊢F:A⟶B\to F=\left\{x\in \left(A\times B\right)|F\left(1^{st}\left(x\right)\right)=2^{nd}\left(x\right)\right\}$$