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

Metamath Proof Explorer

Theorem xpprsng

Description: The Cartesian product of an unordered pair and a singleton. (Contributed by AV, 20-May-2019)

Ref Expression
Assertion xpprsng ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ U → A B × C = A C B C

Proof

Step Hyp Ref Expression
1 df-pr ⊢ A B = A ∪ B
2 1 xpeq1i ⊢ A B × C = A ∪ B × C
3 xpsng ⊢ A ∈ V ∧ C ∈ U → A × C = A C
4 3 3adant2 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ U → A × C = A C
5 xpsng ⊢ B ∈ W ∧ C ∈ U → B × C = B C
6 5 3adant1 ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ U → B × C = B C
7 4 6 uneq12d ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ U → A × C ∪ B × C = A C ∪ B C
8 xpundir ⊢ A ∪ B × C = A × C ∪ B × C
9 df-pr ⊢ A C B C = A C ∪ B C
10 7 8 9 3eqtr4g ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ U → A ∪ B × C = A C B C
11 2 10 eqtrid ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ U → A B × C = A C B C