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 A V B W A B A

Proof

Step Hyp Ref Expression
1 ovexd A V B W A B V
2 snex A V
3 2 a1i A V B W A V
4 simpl A V B W A V
5 4 a1d A V B W x A B A V
6 2 a1i A V A V
7 6 anim1ci A V B W B W A V
8 xpexg B W A V B × A V
9 7 8 syl A V B W B × A V
10 9 a1d A V B W y A B × A V
11 velsn y A y = A
12 11 a1i A V B W y A y = A
13 elmapg A V B W x A B x : B A
14 6 13 sylan A V B W x A B x : B A
15 fconst2g A V x : B A x = B × A
16 15 adantr A V B W x : B A x = B × A
17 14 16 bitr2d A V B W x = B × A x A B
18 12 17 anbi12d A V B W y A x = B × A y = A x A B
19 ancom y = A x A B x A B y = A
20 18 19 bitr2di A V B W x A B y = A y A x = B × A
21 1 3 5 10 20 en2d A V B W A B A