Theorem fmptsnxp

Description: Maps-to notation and Cartesian product for a singleton function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	fmptsnxp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = ( { 𝐴 } × { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		xpsng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } × { 𝐵 } ) = { ⟨ 𝐴 , 𝐵 ⟩ } )
2		fmptsn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )
3	1 2	eqtr2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) = ( { 𝐴 } × { 𝐵 } ) )