This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpprsng

Description: The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019)

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

Proof

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