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

Metamath Proof Explorer

Theorem elpwi2

Description: Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof shortened by Wolf Lammen, 26-May-2024)

Ref Expression
Hypotheses elpwi2.1 ⊢ B ∈ V
elpwi2.2 ⊢ A ⊆ B
Assertion elpwi2 ⊢ A ∈ 𝒫 B

Proof

Step Hyp Ref Expression
1 elpwi2.1 ⊢ B ∈ V
2 elpwi2.2 ⊢ A ⊆ B
3 1 elexi ⊢ B ∈ V
4 3 elpw2 ⊢ A ∈ 𝒫 B ↔ A ⊆ B
5 2 4 mpbir ⊢ A ∈ 𝒫 B