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

Metamath Proof Explorer

Theorem elpwd

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses elpwd.1 ⊢ φ → A ∈ V
elpwd.2 ⊢ φ → A ⊆ B
Assertion elpwd ⊢ φ → A ∈ 𝒫 B

Proof

Step Hyp Ref Expression
1 elpwd.1 ⊢ φ → A ∈ V
2 elpwd.2 ⊢ φ → A ⊆ B
3 elpwg ⊢ A ∈ V → A ∈ 𝒫 B ↔ A ⊆ B
4 1 3 syl ⊢ φ → A ∈ 𝒫 B ↔ A ⊆ B
5 2 4 mpbird ⊢ φ → A ∈ 𝒫 B