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

Metamath Proof Explorer

Theorem dmpropg

Description: The domain of an unordered pair of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion dmpropg ⊢ B ∈ V ∧ D ∈ W → dom ⁡ A B C D = A C

Proof

Step Hyp Ref Expression
1 dmsnopg ⊢ B ∈ V → dom ⁡ A B = A
2 dmsnopg ⊢ D ∈ W → dom ⁡ C D = C
3 uneq12 ⊢ dom ⁡ A B = A ∧ dom ⁡ C D = C → dom ⁡ A B ∪ dom ⁡ C D = A ∪ C
4 1 2 3 syl2an ⊢ B ∈ V ∧ D ∈ W → dom ⁡ A B ∪ dom ⁡ C D = A ∪ C
5 df-pr ⊢ A B C D = A B ∪ C D
6 5 dmeqi ⊢ dom ⁡ A B C D = dom ⁡ A B ∪ C D
7 dmun ⊢ dom ⁡ A B ∪ C D = dom ⁡ A B ∪ dom ⁡ C D
8 6 7 eqtri ⊢ dom ⁡ A B C D = dom ⁡ A B ∪ dom ⁡ C D
9 df-pr ⊢ A C = A ∪ C
10 4 8 9 3eqtr4g ⊢ B ∈ V ∧ D ∈ W → dom ⁡ A B C D = A C