Theorem xpprsng

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

	Ref	Expression
Assertion	xpprsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 , 𝐵 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2	1	xpeq1i	⊢ ( { 𝐴 , 𝐵 } × { 𝐶 } ) = ( ( { 𝐴 } ∪ { 𝐵 } ) × { 𝐶 } )
3		xpsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
4	3	3adant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ } )
5		xpsng	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐵 } × { 𝐶 } ) = { ⟨ 𝐵 , 𝐶 ⟩ } )
6	5	3adant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐵 } × { 𝐶 } ) = { ⟨ 𝐵 , 𝐶 ⟩ } )
7	4 6	uneq12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( ( { 𝐴 } × { 𝐶 } ) ∪ ( { 𝐵 } × { 𝐶 } ) ) = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) )
8		xpundir	⊢ ( ( { 𝐴 } ∪ { 𝐵 } ) × { 𝐶 } ) = ( ( { 𝐴 } × { 𝐶 } ) ∪ ( { 𝐵 } × { 𝐶 } ) )
9		df-pr	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐶 ⟩ } )
10	7 8 9	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( ( { 𝐴 } ∪ { 𝐵 } ) × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } )
11	2 10	syl5eq	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑈 ) → ( { 𝐴 , 𝐵 } × { 𝐶 } ) = { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐶 ⟩ } )