Theorem elintab

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

	Ref	Expression
Hypothesis	inteqab.1	$$⊢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		inteqab.1	$$⊢A\in \mathrm{V}$$
2	1	elint	$$⊢A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall y\left(y\in \left\{x|\phi \right\}\to A\in y\right)$$
3		nfsab1	$$⊢Ⅎxy\in \left\{x|\phi \right\}$$
4		nfv	$$⊢ℲxA\in y$$
5	3 4	nfim	$$⊢Ⅎx\left(y\in \left\{x|\phi \right\}\to A\in y\right)$$
6		nfv	$$⊢Ⅎy\left(\phi \to A\in x\right)$$
7		eleq1w	$$⊢y=x\to \left(y\in \left\{x|\phi \right\}\leftrightarrow x\in \left\{x|\phi \right\}\right)$$
8		abid	$$⊢x\in \left\{x|\phi \right\}\leftrightarrow \phi$$
9	7 8	bitrdi	$$⊢y=x\to \left(y\in \left\{x|\phi \right\}\leftrightarrow \phi \right)$$
10		eleq2w	$$⊢y=x\to \left(A\in y\leftrightarrow A\in x\right)$$
11	9 10	imbi12d	$$⊢y=x\to \left(\left(y\in \left\{x|\phi \right\}\to A\in y\right)\leftrightarrow \left(\phi \to A\in x\right)\right)$$
12	5 6 11	cbvalv1	$$⊢\forall y\left(y\in \left\{x|\phi \right\}\to A\in y\right)\leftrightarrow \forall x\left(\phi \to A\in x\right)$$
13	2 12	bitri	$$⊢A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\in x\right)$$