Theorem elintabg

Description: Two ways of saying a set is an element of the intersection of a class. (Contributed by NM, 30-Aug-1993) Put in closed form. (Revised by RP, 13-Aug-2020)

	Ref	Expression
Assertion	elintabg	$$⊢A\in V\to \left(A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\in x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elintg	$$⊢A\in V\to \left(A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall y\in \left\{x|\phi \right\}A\in y\right)$$
2		eleq2w	$$⊢y=x\to \left(A\in y\leftrightarrow A\in x\right)$$
3	2	ralab2	$$⊢\forall y\in \left\{x|\phi \right\}A\in y\leftrightarrow \forall x\left(\phi \to A\in x\right)$$
4	1 3	bitrdi	$$⊢A\in V\to \left(A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\in x\right)\right)$$