Theorem xpsnprg

Description: The Cartesian product of a singleton and an unordered pair. (Contributed by AV, 21-Aug-2026)

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

Proof

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