Theorem xpsng

Description: The Cartesian product of two singletons is the singleton consisting in the associated ordered pair. (Contributed by Mario Carneiro, 30-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		fconstg	$$⊢B\in W\to \left(\left\{A\right\}\times \left\{B\right\}\right):\left\{A\right\}⟶\left\{B\right\}$$
2	1	adantl	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left\{A\right\}\times \left\{B\right\}\right):\left\{A\right\}⟶\left\{B\right\}$$
3		fsng	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left(\left\{A\right\}\times \left\{B\right\}\right):\left\{A\right\}⟶\left\{B\right\}\leftrightarrow \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}\right)$$
4	2 3	mpbid	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{A\right\}\times \left\{B\right\}=\left\{⟨A,B⟩\right\}$$