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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		funcnvsn	⊢ Fun ◡ { ⟨ 𝐵 , 𝐴 ⟩ }
2		cnvsng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ◡ { ⟨ 𝐵 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } )
3	2	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ { ⟨ 𝐵 , 𝐴 ⟩ } = { ⟨ 𝐴 , 𝐵 ⟩ } )
4	3	funeqd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( Fun ◡ { ⟨ 𝐵 , 𝐴 ⟩ } ↔ Fun { ⟨ 𝐴 , 𝐵 ⟩ } ) )
5	1 4	mpbii	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Fun { ⟨ 𝐴 , 𝐵 ⟩ } )