Theorem dmprop

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

	Ref	Expression
Hypotheses	dmsnop.1	⊢ 𝐵 ∈ V
	dmprop.1	⊢ 𝐷 ∈ V
Assertion	dmprop	⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐴 , 𝐶 }

Proof

Step	Hyp	Ref	Expression
1		dmsnop.1	⊢ 𝐵 ∈ V
2		dmprop.1	⊢ 𝐷 ∈ V
3		dmpropg	⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ) → dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐴 , 𝐶 } )
4	1 2 3	mp2an	⊢ dom { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = { 𝐴 , 𝐶 }