Theorem pw2en

Description: The power set of a set is equinumerous to set exponentiation with a base of ordinal 2. Proposition 10.44 of TakeutiZaring p. 96. This is Metamath 100 proof #52. (Contributed by NM, 29-Jan-2004) (Proof shortened by Mario Carneiro, 1-Jul-2015)

	Ref	Expression
Hypothesis	pw2en.1	⊢ 𝐴 ∈ V
Assertion	pw2en	⊢ 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		pw2en.1	⊢ 𝐴 ∈ V
2		pw2eng	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
3	1 2	ax-mp	⊢ 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 )