This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 } )