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 } )