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	⊢ 𝐴 ∈ V
	funsn.2	⊢ 𝐵 ∈ V
Assertion	funsn	⊢ Fun { ⟨ 𝐴 , 𝐵 ⟩ }

Proof

Step	Hyp	Ref	Expression
1		funsn.1	⊢ 𝐴 ∈ V
2		funsn.2	⊢ 𝐵 ∈ V
3		funsng	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )
4	1 2 3	mp2an	⊢ Fun { ⟨ 𝐴 , 𝐵 ⟩ }