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	$$⊢A\in \mathrm{V}$$
Assertion	pw2en	$$⊢𝒫A\approx \left({2_{𝑜}}^A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pw2en.1	$$⊢A\in \mathrm{V}$$
2		pw2eng	$$⊢A\in \mathrm{V}\to 𝒫A\approx \left({2_{𝑜}}^A\right)$$
3	1 2	ax-mp	$$⊢𝒫A\approx \left({2_{𝑜}}^A\right)$$