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


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