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 A V x A | φ V

Proof

Step Hyp Ref Expression
1 rabelpw A V x A | φ 𝒫 A
2 1 elexd A V x A | φ V