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

Metamath Proof Explorer

Theorem dmpropg

Description: The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion dmpropg 
|- ( ( B e. V /\ D e. W ) -> dom { <. A , B >. , <. C , D >. } = { A , C } )

Proof

Step Hyp Ref Expression
1 dmsnopg 
 |-  ( B e. V -> dom { <. A , B >. } = { A } )
2 dmsnopg 
 |-  ( D e. W -> dom { <. C , D >. } = { C } )
3 uneq12 
 |-  ( ( dom { <. A , B >. } = { A } /\ dom { <. C , D >. } = { C } ) -> ( dom { <. A , B >. } u. dom { <. C , D >. } ) = ( { A } u. { C } ) )
4 1 2 3 syl2an 
 |-  ( ( B e. V /\ D e. W ) -> ( dom { <. A , B >. } u. dom { <. C , D >. } ) = ( { A } u. { C } ) )
5 df-pr 
 |-  { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
6 5 dmeqi 
 |-  dom { <. A , B >. , <. C , D >. } = dom ( { <. A , B >. } u. { <. C , D >. } )
7 dmun 
 |-  dom ( { <. A , B >. } u. { <. C , D >. } ) = ( dom { <. A , B >. } u. dom { <. C , D >. } )
8 6 7 eqtri 
 |-  dom { <. A , B >. , <. C , D >. } = ( dom { <. A , B >. } u. dom { <. C , D >. } )
9 df-pr 
 |-  { A , C } = ( { A } u. { C } )
10 4 8 9 3eqtr4g 
 |-  ( ( B e. V /\ D e. W ) -> dom { <. A , B >. , <. C , D >. } = { A , C } )