Theorem dmprop

Description: The domain of an unordered pair of ordered pairs. (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Hypotheses	dmsnop.1	|- B e. _V
	dmprop.1	|- D e. _V
Assertion	dmprop	|- dom { <. A , B >. , <. C , D >. } = { A , C }

Proof

Step	Hyp	Ref	Expression
1		dmsnop.1	|- B e. _V
2		dmprop.1	|- D e. _V
3		dmpropg	|- ( ( B e. _V /\ D e. _V ) -> dom { <. A , B >. , <. C , D >. } = { A , C } )
4	1 2 3	mp2an	|- dom { <. A , B >. , <. C , D >. } = { A , C }