Theorem fmptsnxp

Description: Maps-to notation and Cartesian product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

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