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

Metamath Proof Explorer

Theorem rabelpw

Description: A restricted class abstraction is an element of the power set of its restricting set. (Contributed by AV, 9-Oct-2023)

Ref Expression
Assertion rabelpw ⊢ A ∈ V → x ∈ A | φ ∈ 𝒫 A

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ x ∈ A | φ ⊆ A
2 elpw2g ⊢ A ∈ V → x ∈ A | φ ∈ 𝒫 A ↔ x ∈ A | φ ⊆ A
3 1 2 mpbiri ⊢ A ∈ V → x ∈ A | φ ∈ 𝒫 A