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 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { 〈 𝐴 , 𝐵 〉 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg | ⊢ ( 𝐵 ∈ 𝑊 → ( { 𝐴 } × { 𝐵 } ) : { 𝐴 } ⟶ { 𝐵 } ) | |
2 | 1 | adantl | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) : { 𝐴 } ⟶ { 𝐵 } ) |
3 | fsng | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { 𝐴 } × { 𝐵 } ) : { 𝐴 } ⟶ { 𝐵 } ↔ ( { 𝐴 } × { 𝐵 } ) = { 〈 𝐴 , 𝐵 〉 } ) ) | |
4 | 2 3 | mpbid | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { 〈 𝐴 , 𝐵 〉 } ) |