Description: Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pwex.1 | ⊢ 𝐴 ∈ V | |
Assertion | pwex | ⊢ 𝒫 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwex.1 | ⊢ 𝐴 ∈ V | |
2 | pwexg | ⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V ) | |
3 | 1 2 | ax-mp | ⊢ 𝒫 𝐴 ∈ V |