Theorem fnsng

Description: Functionality and domain of the singleton of an ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	fnsng	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } Fn { A } )

Proof

Step	Hyp	Ref	Expression
1		funsng	|- ( ( A e. V /\ B e. W ) -> Fun { <. A , B >. } )
2		dmsnopg	|- ( B e. W -> dom { <. A , B >. } = { A } )
3	2	adantl	|- ( ( A e. V /\ B e. W ) -> dom { <. A , B >. } = { A } )
4		df-fn	|- ( { <. A , B >. } Fn { A } <-> ( Fun { <. A , B >. } /\ dom { <. A , B >. } = { A } ) )
5	1 3 4	sylanbrc	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } Fn { A } )