Theorem funop1

Description: A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) (Avoid depending on this detail.)

	Ref	Expression
Assertion	funop1	$$⊢\exists x\exists yF=⟨x,y⟩\to \left(\mathrm{Fun}F\leftrightarrow \exists x\exists yF=\left\{⟨x,y⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		opeq12	$$⊢\left(x=v\wedge y=w\right)\to ⟨x,y⟩=⟨v,w⟩$$
2	1	eqeq2d	$$⊢\left(x=v\wedge y=w\right)\to \left(F=⟨x,y⟩\leftrightarrow F=⟨v,w⟩\right)$$
3	2	cbvex2vw	$$⊢\exists x\exists yF=⟨x,y⟩\leftrightarrow \exists v\exists wF=⟨v,w⟩$$
4		vex	$$⊢v\in \mathrm{V}$$
5		vex	$$⊢w\in \mathrm{V}$$
6	4 5	funopsn	$$⊢\left(\mathrm{Fun}F\wedge F=⟨v,w⟩\right)\to \exists a\left(v=\left\{a\right\}\wedge F=\left\{⟨a,a⟩\right\}\right)$$
7		vex	$$⊢a\in \mathrm{V}$$
8		opeq12	$$⊢\left(x=a\wedge y=a\right)\to ⟨x,y⟩=⟨a,a⟩$$
9	8	sneqd	$$⊢\left(x=a\wedge y=a\right)\to \left\{⟨x,y⟩\right\}=\left\{⟨a,a⟩\right\}$$
10	9	eqeq2d	$$⊢\left(x=a\wedge y=a\right)\to \left(F=\left\{⟨x,y⟩\right\}\leftrightarrow F=\left\{⟨a,a⟩\right\}\right)$$
11	7 7 10	spc2ev	$$⊢F=\left\{⟨a,a⟩\right\}\to \exists x\exists yF=\left\{⟨x,y⟩\right\}$$
12	11	adantl	$$⊢\left(v=\left\{a\right\}\wedge F=\left\{⟨a,a⟩\right\}\right)\to \exists x\exists yF=\left\{⟨x,y⟩\right\}$$
13	12	exlimiv	$$⊢\exists a\left(v=\left\{a\right\}\wedge F=\left\{⟨a,a⟩\right\}\right)\to \exists x\exists yF=\left\{⟨x,y⟩\right\}$$
14	6 13	syl	$$⊢\left(\mathrm{Fun}F\wedge F=⟨v,w⟩\right)\to \exists x\exists yF=\left\{⟨x,y⟩\right\}$$
15	14	expcom	$$⊢F=⟨v,w⟩\to \left(\mathrm{Fun}F\to \exists x\exists yF=\left\{⟨x,y⟩\right\}\right)$$
16		vex	$$⊢x\in \mathrm{V}$$
17		vex	$$⊢y\in \mathrm{V}$$
18	16 17	funsn	$$⊢\mathrm{Fun}\left\{⟨x,y⟩\right\}$$
19		funeq	$$⊢F=\left\{⟨x,y⟩\right\}\to \left(\mathrm{Fun}F\leftrightarrow \mathrm{Fun}\left\{⟨x,y⟩\right\}\right)$$
20	18 19	mpbiri	$$⊢F=\left\{⟨x,y⟩\right\}\to \mathrm{Fun}F$$
21	20	exlimivv	$$⊢\exists x\exists yF=\left\{⟨x,y⟩\right\}\to \mathrm{Fun}F$$
22	15 21	impbid1	$$⊢F=⟨v,w⟩\to \left(\mathrm{Fun}F\leftrightarrow \exists x\exists yF=\left\{⟨x,y⟩\right\}\right)$$
23	22	exlimivv	$$⊢\exists v\exists wF=⟨v,w⟩\to \left(\mathrm{Fun}F\leftrightarrow \exists x\exists yF=\left\{⟨x,y⟩\right\}\right)$$
24	3 23	sylbi	$$⊢\exists x\exists yF=⟨x,y⟩\to \left(\mathrm{Fun}F\leftrightarrow \exists x\exists yF=\left\{⟨x,y⟩\right\}\right)$$