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	$⊢ (A \in V \land B \in W) \to \{⟨A, B⟩\} = (x \in \{A\} ⟼ B)$

Proof

Step	Hyp	Ref	Expression
1		xpsng	$⊢ (A \in V \land B \in W) \to \{A\} \times \{B\} = \{⟨A, B⟩\}$
2		fconstmpt	$⊢ \{A\} \times \{B\} = (x \in \{A\} ⟼ B)$
3	1 2	eqtr3di	$⊢ (A \in V \land B \in W) \to \{⟨A, B⟩\} = (x \in \{A\} ⟼ B)$