Theorem dmprop

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

	Ref	Expression
Hypotheses	dmsnop.1	$$⊢B\in \mathrm{V}$$
	dmprop.1	$$⊢D\in \mathrm{V}$$
Assertion	dmprop	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{A,C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmsnop.1	$$⊢B\in \mathrm{V}$$
2		dmprop.1	$$⊢D\in \mathrm{V}$$
3		dmpropg	$$⊢\left(B\in \mathrm{V}\wedge D\in \mathrm{V}\right)\to \mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{A,C\right\}$$
4	1 2 3	mp2an	$$⊢\mathrm{dom}\left\{⟨A,B⟩,⟨C,D⟩\right\}=\left\{A,C\right\}$$