Theorem snmapen1

Description: Set exponentiation: a singleton to any set is equinumerous to ordinal 1. (Proposed by BJ, 17-Jul-2022.) (Contributed by AV, 17-Jul-2022)

	Ref	Expression
Assertion	snmapen1	$$⊢\left(A\in V\wedge B\in W\right)\to \left({\left\{A\right\}}^B\right)\approx 1_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		snmapen	$$⊢\left(A\in V\wedge B\in W\right)\to \left({\left\{A\right\}}^B\right)\approx \left\{A\right\}$$
2		ensn1g	$$⊢A\in V\to \left\{A\right\}\approx 1_{𝑜}$$
3	2	adantr	$$⊢\left(A\in V\wedge B\in W\right)\to \left\{A\right\}\approx 1_{𝑜}$$
4		entr	$$⊢\left(\left({\left\{A\right\}}^B\right)\approx \left\{A\right\}\wedge \left\{A\right\}\approx 1_{𝑜}\right)\to \left({\left\{A\right\}}^B\right)\approx 1_{𝑜}$$
5	1 3 4	syl2anc	$$⊢\left(A\in V\wedge B\in W\right)\to \left({\left\{A\right\}}^B\right)\approx 1_{𝑜}$$