Metamath Proof Explorer


Theorem rabexg

Description: Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999) (Proof shortened by BJ, 24-Jul-2025)

Ref Expression
Assertion rabexg ( 𝐴𝑉 → { 𝑥𝐴𝜑 } ∈ V )

Proof

Step Hyp Ref Expression
1 rabelpw ( 𝐴𝑉 → { 𝑥𝐴𝜑 } ∈ 𝒫 𝐴 )
2 1 elexd ( 𝐴𝑉 → { 𝑥𝐴𝜑 } ∈ V )