Theorem xpsng

Description: The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fconstg	|- ( B e. W -> ( { A } X. { B } ) : { A } --> { B } )
2	1	adantl	|- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) : { A } --> { B } )
3		fsng	|- ( ( A e. V /\ B e. W ) -> ( ( { A } X. { B } ) : { A } --> { B } <-> ( { A } X. { B } ) = { <. A , B >. } ) )
4	2 3	mpbid	|- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } )