# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({\left\{{A}\right\}}^{{B}}\right)\approx \left\{{A}\right\}$

### Proof

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