Theorem funsng

Description: A singleton of an ordered pair is a function. Theorem 10.5 of Quine p. 65. (Contributed by NM, 28-Jun-2011)

	Ref	Expression
Assertion	funsng	$$⊢\left(A\in V\wedge B\in W\right)\to \mathrm{Fun}\left\{⟨A,B⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funcnvsn	$$⊢\mathrm{Fun}{\left\{⟨B,A⟩\right\}}^{-1}$$
2		cnvsng	$$⊢\left(B\in W\wedge A\in V\right)\to {\left\{⟨B,A⟩\right\}}^{-1}=\left\{⟨A,B⟩\right\}$$
3	2	ancoms	$$⊢\left(A\in V\wedge B\in W\right)\to {\left\{⟨B,A⟩\right\}}^{-1}=\left\{⟨A,B⟩\right\}$$
4	3	funeqd	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\mathrm{Fun}{\left\{⟨B,A⟩\right\}}^{-1}\leftrightarrow \mathrm{Fun}\left\{⟨A,B⟩\right\}\right)$$
5	1 4	mpbii	$$⊢\left(A\in V\wedge B\in W\right)\to \mathrm{Fun}\left\{⟨A,B⟩\right\}$$