snmapen

Description: Set exponentiation: a singleton to any set is equinumerous to that singleton. (Contributed by NM, 17-Dec-2003) (Revised by AV, 17-Jul-2022)

		Ref	Expression
	Assertion	snmapen	$⊢ (A \in V \land B \in W) \to ({\{A\}}^{B}) \approx \{A\}$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$⊢ (A \in V \land B \in W) \to {\{A\}}^{B} \in V$
2		snex	$⊢ \{A\} \in V$
3	2	a1i	$⊢ (A \in V \land B \in W) \to \{A\} \in V$
4		simpl	$⊢ (A \in V \land B \in W) \to A \in V$
5	4	a1d	$⊢ (A \in V \land B \in W) \to (x \in ({\{A\}}^{B}) \to A \in V)$
6	2	a1i	$⊢ A \in V \to \{A\} \in V$
7	6	anim1ci	$⊢ (A \in V \land B \in W) \to (B \in W \land \{A\} \in V)$
8		xpexg	$⊢ (B \in W \land \{A\} \in V) \to B \times \{A\} \in V$
9	7 8	syl	$⊢ (A \in V \land B \in W) \to B \times \{A\} \in V$
10	9	a1d	$⊢ (A \in V \land B \in W) \to (y \in \{A\} \to B \times \{A\} \in V)$
11		velsn	$⊢ y \in \{A\} \leftrightarrow y = A$
12	11	a1i	$⊢ (A \in V \land B \in W) \to (y \in \{A\} \leftrightarrow y = A)$
13		elmapg	$⊢ (\{A\} \in V \land B \in W) \to (x \in ({\{A\}}^{B}) \leftrightarrow x : B ⟶ \{A\})$
14	6 13	sylan	$⊢ (A \in V \land B \in W) \to (x \in ({\{A\}}^{B}) \leftrightarrow x : B ⟶ \{A\})$
15		fconst2g	$⊢ A \in V \to (x : B ⟶ \{A\} \leftrightarrow x = B \times \{A\})$
16	15	adantr	$⊢ (A \in V \land B \in W) \to (x : B ⟶ \{A\} \leftrightarrow x = B \times \{A\})$
17	14 16	bitr2d	$⊢ (A \in V \land B \in W) \to (x = B \times \{A\} \leftrightarrow x \in ({\{A\}}^{B}))$
18	12 17	anbi12d	$⊢ (A \in V \land B \in W) \to ((y \in \{A\} \land x = B \times \{A\}) \leftrightarrow (y = A \land x \in ({\{A\}}^{B})))$
19		ancom	$⊢ (y = A \land x \in ({\{A\}}^{B})) \leftrightarrow (x \in ({\{A\}}^{B}) \land y = A)$
20	18 19	bitr2di	$⊢ (A \in V \land B \in W) \to ((x \in ({\{A\}}^{B}) \land y = A) \leftrightarrow (y \in \{A\} \land x = B \times \{A\}))$
21	1 3 5 10 20	en2d	$⊢ (A \in V \land B \in W) \to ({\{A\}}^{B}) \approx \{A\}$

Metamath Proof Explorer

Theorem snmapen

Proof