Theorem intexab

Description: The intersection of a nonempty class abstraction exists. (Contributed by NM, 21-Oct-2003)

	Ref	Expression
Assertion	intexab	$$⊢\exists x\phi \leftrightarrow \bigcap \left\{x|\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		abn0	$$⊢\left\{x|\phi \right\}\ne \varnothing \leftrightarrow \exists x\phi$$
2		intex	$$⊢\left\{x|\phi \right\}\ne \varnothing \leftrightarrow \bigcap \left\{x|\phi \right\}\in \mathrm{V}$$
3	1 2	bitr3i	$$⊢\exists x\phi \leftrightarrow \bigcap \left\{x|\phi \right\}\in \mathrm{V}$$