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→AB≈A

Proof

Step Hyp Ref Expression
1 ovexd ⊢A∈V∧B∈W→AB∈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∈AB→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∈AB↔x:B⟶A
14 6 13 sylan ⊢A∈V∧B∈W→x∈AB↔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∈AB
18 12 17 anbi12d ⊢A∈V∧B∈W→y∈A∧x=B×A↔y=A∧x∈AB
19 ancom ⊢y=A∧x∈AB↔x∈AB∧y=A
20 18 19 bitr2di ⊢A∈V∧B∈W→x∈AB∧y=A↔y∈A∧x=B×A
21 1 3 5 10 20 en2d ⊢A∈V∧B∈W→AB≈A