Theorem zfausab

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

	Ref	Expression
Hypothesis	zfausab.1	|- A e. _V
Assertion	zfausab	|- { x | ( x e. A /\ ph ) } e. _V

Proof

Step	Hyp	Ref	Expression
1		zfausab.1	|- A e. _V
2		ssab2	|- { x | ( x e. A /\ ph ) } C_ A
3	1 2	ssexi	|- { x | ( x e. A /\ ph ) } e. _V