Metamath Proof Explorer


Theorem zfausab

Description: Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994)

Ref Expression
Hypothesis zfausab.1 𝐴 ∈ V
Assertion zfausab { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } ∈ V

Proof

Step Hyp Ref Expression
1 zfausab.1 𝐴 ∈ V
2 ssab2 { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } ⊆ 𝐴
3 1 2 ssexi { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } ∈ V