Theorem fsng

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 26-Oct-2012)

	Ref	Expression
Assertion	fsng	$$⊢\left(A\in C\wedge B\in D\right)\to \left(F:\left\{A\right\}⟶\left\{B\right\}\leftrightarrow F=\left\{⟨A,B⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢a=A\to \left\{a\right\}=\left\{A\right\}$$
2	1	feq2d	$$⊢a=A\to \left(F:\left\{a\right\}⟶\left\{b\right\}\leftrightarrow F:\left\{A\right\}⟶\left\{b\right\}\right)$$
3		opeq1	$$⊢a=A\to ⟨a,b⟩=⟨A,b⟩$$
4	3	sneqd	$$⊢a=A\to \left\{⟨a,b⟩\right\}=\left\{⟨A,b⟩\right\}$$
5	4	eqeq2d	$$⊢a=A\to \left(F=\left\{⟨a,b⟩\right\}\leftrightarrow F=\left\{⟨A,b⟩\right\}\right)$$
6	2 5	bibi12d	$$⊢a=A\to \left(\left(F:\left\{a\right\}⟶\left\{b\right\}\leftrightarrow F=\left\{⟨a,b⟩\right\}\right)\leftrightarrow \left(F:\left\{A\right\}⟶\left\{b\right\}\leftrightarrow F=\left\{⟨A,b⟩\right\}\right)\right)$$
7		sneq	$$⊢b=B\to \left\{b\right\}=\left\{B\right\}$$
8	7	feq3d	$$⊢b=B\to \left(F:\left\{A\right\}⟶\left\{b\right\}\leftrightarrow F:\left\{A\right\}⟶\left\{B\right\}\right)$$
9		opeq2	$$⊢b=B\to ⟨A,b⟩=⟨A,B⟩$$
10	9	sneqd	$$⊢b=B\to \left\{⟨A,b⟩\right\}=\left\{⟨A,B⟩\right\}$$
11	10	eqeq2d	$$⊢b=B\to \left(F=\left\{⟨A,b⟩\right\}\leftrightarrow F=\left\{⟨A,B⟩\right\}\right)$$
12	8 11	bibi12d	$$⊢b=B\to \left(\left(F:\left\{A\right\}⟶\left\{b\right\}\leftrightarrow F=\left\{⟨A,b⟩\right\}\right)\leftrightarrow \left(F:\left\{A\right\}⟶\left\{B\right\}\leftrightarrow F=\left\{⟨A,B⟩\right\}\right)\right)$$
13		vex	$$⊢a\in \mathrm{V}$$
14		vex	$$⊢b\in \mathrm{V}$$
15	13 14	fsn	$$⊢F:\left\{a\right\}⟶\left\{b\right\}\leftrightarrow F=\left\{⟨a,b⟩\right\}$$
16	6 12 15	vtocl2g	$$⊢\left(A\in C\wedge B\in D\right)\to \left(F:\left\{A\right\}⟶\left\{B\right\}\leftrightarrow F=\left\{⟨A,B⟩\right\}\right)$$