Theorem fmptsn

Description: Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by Stefan O'Rear, 28-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fconstmpt	|- ( { A } X. { B } ) = ( x e. { A } |-> B )
2		xpsng	|- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } )
3	1 2	syl5reqr	|- ( ( A e. V /\ B e. W ) -> { <. A , B >. } = ( x e. { A } |-> B ) )