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	|- ( ( A e. V /\ B e. W ) -> Fun { <. A , B >. } )

Proof

Step	Hyp	Ref	Expression
1		funcnvsn	|- Fun `' { <. B , A >. }
2		cnvsng	|- ( ( B e. W /\ A e. V ) -> `' { <. B , A >. } = { <. A , B >. } )
3	2	ancoms	|- ( ( A e. V /\ B e. W ) -> `' { <. B , A >. } = { <. A , B >. } )
4	3	funeqd	|- ( ( A e. V /\ B e. W ) -> ( Fun `' { <. B , A >. } <-> Fun { <. A , B >. } ) )
5	1 4	mpbii	|- ( ( A e. V /\ B e. W ) -> Fun { <. A , B >. } )