Theorem elintab

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993)

	Ref	Expression
Hypothesis	elintab.ex	$$⊢A\in \mathrm{V}$$
Assertion	elintab	$$⊢A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		elintab.ex	$$⊢A\in \mathrm{V}$$
2		elintabg	$$⊢A\in \mathrm{V}\to \left(A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\in x\right)\right)$$
3	1 2	ax-mp	$$⊢A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\in x\right)$$