Theorem zfausab

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

	Ref	Expression
Hypothesis	zfausab.1	$$⊢A\in \mathrm{V}$$
Assertion	zfausab	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		zfausab.1	$$⊢A\in \mathrm{V}$$
2		ssab2	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\subseteq A$$
3	1 2	ssexi	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$