Theorem xpsnprg

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

	Ref	Expression
Assertion	xpsnprg	$$⊢\left(A\in V\wedge B\in W\wedge C\in U\right)\to \left\{A\right\}\times \left\{B,C\right\}=\left\{⟨A,B⟩,⟨A,C⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{B,C\right\}=\left\{B\right\}\cup \left\{C\right\}$$
2	1	xpeq2i	$$⊢\left\{A\right\}\times \left\{B,C\right\}=\left\{A\right\}\times \left(\left\{B\right\}\cup \left\{C\right\}\right)$$
3		xpsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$
4	3	3adant3	$$⊢\left(A\in V\wedge B\in W\wedge C\in U\right)\to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$
5		xpsng	$$⊢\left(A\in V\wedge C\in U\right)\to \left\{A\right\}\times \left\{C\right\}=\left\{⟨A,C⟩\right\}$$
6	5	3adant2	$$⊢\left(A\in V\wedge B\in W\wedge C\in U\right)\to \left\{A\right\}\times \left\{C\right\}=\left\{⟨A,C⟩\right\}$$
7	4 6	uneq12d	$$⊢\left(A\in V\wedge B\in W\wedge C\in U\right)\to \left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)=\left\{⟨A,B⟩\right\}\cup \left\{⟨A,C⟩\right\}$$
8		xpundi	$$⊢\left\{A\right\}\times \left(\left\{B\right\}\cup \left\{C\right\}\right)=\left(\left\{A\right\}\times \left\{B\right\}\right)\cup \left(\left\{A\right\}\times \left\{C\right\}\right)$$
9		df-pr	$$⊢\left\{⟨A,B⟩,⟨A,C⟩\right\}=\left\{⟨A,B⟩\right\}\cup \left\{⟨A,C⟩\right\}$$
10	7 8 9	3eqtr4g	$$⊢\left(A\in V\wedge B\in W\wedge C\in U\right)\to \left\{A\right\}\times \left(\left\{B\right\}\cup \left\{C\right\}\right)=\left\{⟨A,B⟩,⟨A,C⟩\right\}$$
11	2 10	eqtrid	$$⊢\left(A\in V\wedge B\in W\wedge C\in U\right)\to \left\{A\right\}\times \left\{B,C\right\}=\left\{⟨A,B⟩,⟨A,C⟩\right\}$$