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 e. V /\ B e. W ) -> ( { A } ^m B ) ~~ { A } )

Proof

Step	Hyp	Ref	Expression
1		ovexd	|- ( ( A e. V /\ B e. W ) -> ( { A } ^m B ) e. _V )
2		snex	|- { A } e. _V
3	2	a1i	|- ( ( A e. V /\ B e. W ) -> { A } e. _V )
4		simpl	|- ( ( A e. V /\ B e. W ) -> A e. V )
5	4	a1d	|- ( ( A e. V /\ B e. W ) -> ( x e. ( { A } ^m B ) -> A e. V ) )
6	2	a1i	|- ( A e. V -> { A } e. _V )
7	6	anim1ci	|- ( ( A e. V /\ B e. W ) -> ( B e. W /\ { A } e. _V ) )
8		xpexg	|- ( ( B e. W /\ { A } e. _V ) -> ( B X. { A } ) e. _V )
9	7 8	syl	|- ( ( A e. V /\ B e. W ) -> ( B X. { A } ) e. _V )
10	9	a1d	|- ( ( A e. V /\ B e. W ) -> ( y e. { A } -> ( B X. { A } ) e. _V ) )
11		velsn	|- ( y e. { A } <-> y = A )
12	11	a1i	|- ( ( A e. V /\ B e. W ) -> ( y e. { A } <-> y = A ) )
13		elmapg	|- ( ( { A } e. _V /\ B e. W ) -> ( x e. ( { A } ^m B ) <-> x : B --> { A } ) )
14	6 13	sylan	|- ( ( A e. V /\ B e. W ) -> ( x e. ( { A } ^m B ) <-> x : B --> { A } ) )
15		fconst2g	|- ( A e. V -> ( x : B --> { A } <-> x = ( B X. { A } ) ) )
16	15	adantr	|- ( ( A e. V /\ B e. W ) -> ( x : B --> { A } <-> x = ( B X. { A } ) ) )
17	14 16	bitr2d	|- ( ( A e. V /\ B e. W ) -> ( x = ( B X. { A } ) <-> x e. ( { A } ^m B ) ) )
18	12 17	anbi12d	|- ( ( A e. V /\ B e. W ) -> ( ( y e. { A } /\ x = ( B X. { A } ) ) <-> ( y = A /\ x e. ( { A } ^m B ) ) ) )
19		ancom	|- ( ( y = A /\ x e. ( { A } ^m B ) ) <-> ( x e. ( { A } ^m B ) /\ y = A ) )
20	18 19	bitr2di	|- ( ( A e. V /\ B e. W ) -> ( ( x e. ( { A } ^m B ) /\ y = A ) <-> ( y e. { A } /\ x = ( B X. { A } ) ) ) )
21	1 3 5 10 20	en2d	|- ( ( A e. V /\ B e. W ) -> ( { A } ^m B ) ~~ { A } )