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