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

Metamath Proof Explorer

Theorem mapsn

Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Proof shortened by AV, 17-Jul-2022)

	Ref	Expression
Hypotheses	map0.1	$⊢ A \in V$
	map0.2	$⊢ B \in V$
Assertion	mapsn	$⊢ A^{\{B\}} = \{f \| \exists y \in A f = \{⟨B, y⟩\}\}$

Proof

Step	Hyp	Ref	Expression
1		map0.1	$⊢ A \in V$
2		map0.2	$⊢ B \in V$
3		id	$⊢ A \in V \to A \in V$
4	2	a1i	$⊢ A \in V \to B \in V$
5	3 4	mapsnd	$⊢ A \in V \to A^{\{B\}} = \{f \| \exists y \in A f = \{⟨B, y⟩\}\}$
6	1 5	ax-mp	$⊢ A^{\{B\}} = \{f \| \exists y \in A f = \{⟨B, y⟩\}\}$