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

Metamath Proof Explorer

Theorem dmprop

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

Ref Expression
Hypotheses dmsnop.1 ⊢ B ∈ V
dmprop.1 ⊢ D ∈ V
Assertion dmprop ⊢ dom ⁡ A B C D = A C

Proof

Step Hyp Ref Expression
1 dmsnop.1 ⊢ B ∈ V
2 dmprop.1 ⊢ D ∈ V
3 dmpropg ⊢ B ∈ V ∧ D ∈ V → dom ⁡ A B C D = A C
4 1 2 3 mp2an ⊢ dom ⁡ A B C D = A C