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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		fconstg	⊢ ( 𝐵 ∈ 𝑊 → ( { 𝐴 } × { 𝐵 } ) : { 𝐴 } ⟶ { 𝐵 } )
2	1	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) : { 𝐴 } ⟶ { 𝐵 } )
3		fsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { 𝐴 } × { 𝐵 } ) : { 𝐴 } ⟶ { 𝐵 } ↔ ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } ) )
4	2 3	mpbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )