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 elex ⊢ A ∈ V → A ∈ V
5 4 adantr ⊢ A ∈ V ∧ B ∈ W → A ∈ V
6 5 a1d ⊢ A ∈ V ∧ B ∈ W → x ∈ A B → A ∈ V
7 2 a1i ⊢ A ∈ V → A ∈ V
8 7 anim1ci ⊢ A ∈ V ∧ B ∈ W → B ∈ W ∧ A ∈ V
9 xpexg ⊢ B ∈ W ∧ A ∈ V → B × A ∈ V
10 8 9 syl ⊢ A ∈ V ∧ B ∈ W → B × A ∈ V
11 10 a1d ⊢ A ∈ V ∧ B ∈ W → y ∈ A → B × A ∈ V
12 velsn ⊢ y ∈ A ↔ y = A
13 12 a1i ⊢ A ∈ V ∧ B ∈ W → y ∈ A ↔ y = A
14 elmapg ⊢ A ∈ V ∧ B ∈ W → x ∈ A B ↔ x : B ⟶ A
15 7 14 sylan ⊢ A ∈ V ∧ B ∈ W → x ∈ A B ↔ x : B ⟶ A
16 fconst2g ⊢ A ∈ V → x : B ⟶ A ↔ x = B × A
17 16 adantr ⊢ A ∈ V ∧ B ∈ W → x : B ⟶ A ↔ x = B × A
18 15 17 bitr2d ⊢ A ∈ V ∧ B ∈ W → x = B × A ↔ x ∈ A B
19 13 18 anbi12d ⊢ A ∈ V ∧ B ∈ W → y ∈ A ∧ x = B × A ↔ y = A ∧ x ∈ A B
20 ancom ⊢ y = A ∧ x ∈ A B ↔ x ∈ A B ∧ y = A
21 19 20 syl6rbb ⊢ A ∈ V ∧ B ∈ W → x ∈ A B ∧ y = A ↔ y ∈ A ∧ x = B × A
22 1 3 6 11 21 en2d ⊢ A ∈ V ∧ B ∈ W → A B ≈ A