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 ⊢ 𝐵 ∈ 𝑉
elpwi2.2 ⊢ 𝐴 ⊆ 𝐵
Assertion elpwi2 𝐴 ∈ 𝒫 𝐵

Proof

Step Hyp Ref Expression
1 elpwi2.1 ⊢ 𝐵 ∈ 𝑉
2 elpwi2.2 ⊢ 𝐴 ⊆ 𝐵
3 1 elexi ⊢ 𝐵 ∈ V
4 3 elpw2 ⊢ ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 )
5 2 4 mpbir ⊢ 𝐴 ∈ 𝒫 𝐵