This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmptsn

Description: Express a singleton function in maps-to notation. (Contributed by NM, 6-Jun-2006) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by Stefan O'Rear, 28-Feb-2015)

		Ref	Expression
	Assertion	fmptsn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { ⟨ 𝐴 , 𝐵 ⟩ } = ( 𝑥 ∈ { 𝐴 } ↦ 𝐵 ) )

Proof

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