Metamath Proof Explorer


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