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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ≈ { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		ovexd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ∈ V )
2		snex	⊢ { 𝐴 } ∈ V
3	2	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝐴 } ∈ V )
4		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
5	4	a1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) → 𝐴 ∈ 𝑉 ) )
6	2	a1i	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ∈ V )
7	6	anim1ci	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∈ 𝑊 ∧ { 𝐴 } ∈ V ) )
8		xpexg	⊢ ( ( 𝐵 ∈ 𝑊 ∧ { 𝐴 } ∈ V ) → ( 𝐵 × { 𝐴 } ) ∈ V )
9	7 8	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 × { 𝐴 } ) ∈ V )
10	9	a1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑦 ∈ { 𝐴 } → ( 𝐵 × { 𝐴 } ) ∈ V ) )
11		velsn	⊢ ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 )
12	11	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑦 ∈ { 𝐴 } ↔ 𝑦 = 𝐴 ) )
13		elmapg	⊢ ( ( { 𝐴 } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ↔ 𝑥 : 𝐵 ⟶ { 𝐴 } ) )
14	6 13	sylan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ↔ 𝑥 : 𝐵 ⟶ { 𝐴 } ) )
15		fconst2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 : 𝐵 ⟶ { 𝐴 } ↔ 𝑥 = ( 𝐵 × { 𝐴 } ) ) )
16	15	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 : 𝐵 ⟶ { 𝐴 } ↔ 𝑥 = ( 𝐵 × { 𝐴 } ) ) )
17	14 16	bitr2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 = ( 𝐵 × { 𝐴 } ) ↔ 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ) )
18	12 17	anbi12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑦 ∈ { 𝐴 } ∧ 𝑥 = ( 𝐵 × { 𝐴 } ) ) ↔ ( 𝑦 = 𝐴 ∧ 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ) ) )
19		ancom	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ) ↔ ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ∧ 𝑦 = 𝐴 ) )
20	18 19	bitr2di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝑥 ∈ ( { 𝐴 } ↑m 𝐵 ) ∧ 𝑦 = 𝐴 ) ↔ ( 𝑦 ∈ { 𝐴 } ∧ 𝑥 = ( 𝐵 × { 𝐴 } ) ) ) )
21	1 3 5 10 20	en2d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ↑m 𝐵 ) ≈ { 𝐴 } )