Theorem xpsnprg

Description: The Cartesian product of a singleton and an unordered pair. (Contributed by AV, 21-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		df-pr	|- { B , C } = ( { B } u. { C } )
2	1	xpeq2i	|- ( { A } X. { B , C } ) = ( { A } X. ( { B } u. { C } ) )
3		xpsng	|- ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } )
4	3	3adant3	|- ( ( A e. V /\ B e. W /\ C e. U ) -> ( { A } X. { B } ) = { <. A , B >. } )
5		xpsng	|- ( ( A e. V /\ C e. U ) -> ( { A } X. { C } ) = { <. A , C >. } )
6	5	3adant2	|- ( ( A e. V /\ B e. W /\ C e. U ) -> ( { A } X. { C } ) = { <. A , C >. } )
7	4 6	uneq12d	|- ( ( A e. V /\ B e. W /\ C e. U ) -> ( ( { A } X. { B } ) u. ( { A } X. { C } ) ) = ( { <. A , B >. } u. { <. A , C >. } ) )
8		xpundi	|- ( { A } X. ( { B } u. { C } ) ) = ( ( { A } X. { B } ) u. ( { A } X. { C } ) )
9		df-pr	|- { <. A , B >. , <. A , C >. } = ( { <. A , B >. } u. { <. A , C >. } )
10	7 8 9	3eqtr4g	|- ( ( A e. V /\ B e. W /\ C e. U ) -> ( { A } X. ( { B } u. { C } ) ) = { <. A , B >. , <. A , C >. } )
11	2 10	eqtrid	|- ( ( A e. V /\ B e. W /\ C e. U ) -> ( { A } X. { B , C } ) = { <. A , B >. , <. A , C >. } )