Theorem intexrab

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

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

Proof

Step	Hyp	Ref	Expression
1		intexab	$$⊢\exists x\left(x\in A\wedge \phi \right)\leftrightarrow \bigcap \left\{x|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
2		df-rex	$$⊢\exists x\in A\phi \leftrightarrow \exists x\left(x\in A\wedge \phi \right)$$
3		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
4	3	inteqi	$$⊢\bigcap \left\{x\in A|\phi \right\}=\bigcap \left\{x|\left(x\in A\wedge \phi \right)\right\}$$
5	4	eleq1i	$$⊢\bigcap \left\{x\in A|\phi \right\}\in \mathrm{V}\leftrightarrow \bigcap \left\{x|\left(x\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
6	1 2 5	3bitr4i	$$⊢\exists x\in A\phi \leftrightarrow \bigcap \left\{x\in A|\phi \right\}\in \mathrm{V}$$