Theorem elintg

Description: Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003) (Proof shortened by JJ, 26-Jul-2021)

	Ref	Expression
Assertion	elintg	$$⊢A\in V\to \left(A\in \bigcap B\leftrightarrow \forall x\in BA\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢y=A\to \left(y\in x\leftrightarrow A\in x\right)$$
2	1	ralbidv	$$⊢y=A\to \left(\forall x\in By\in x\leftrightarrow \forall x\in BA\in x\right)$$
3		dfint2	$$⊢\bigcap B=\left\{y|\forall x\in By\in x\right\}$$
4	2 3	elab2g	$$⊢A\in V\to \left(A\in \bigcap B\leftrightarrow \forall x\in BA\in x\right)$$