Theorem funsn

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

	Ref	Expression
Hypotheses	funsn.1	$$⊢A\in \mathrm{V}$$
	funsn.2	$$⊢B\in \mathrm{V}$$
Assertion	funsn	$$⊢\mathrm{Fun}\left\{⟨A,B⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funsn.1	$$⊢A\in \mathrm{V}$$
2		funsn.2	$$⊢B\in \mathrm{V}$$
3		funsng	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \mathrm{Fun}\left\{⟨A,B⟩\right\}$$
4	1 2 3	mp2an	$$⊢\mathrm{Fun}\left\{⟨A,B⟩\right\}$$