This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 )