Theorem elinintab

Description: Two ways of saying a set is an element of the intersection of a class with the intersection of a class. (Contributed by RP, 13-Aug-2020)

	Ref	Expression
Assertion	elinintab	$$⊢A\in \left(B\cap \bigcap \left\{x|\phi \right\}\right)\leftrightarrow \left(A\in B\wedge \forall x\left(\phi \to A\in x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elin	$$⊢A\in \left(B\cap \bigcap \left\{x|\phi \right\}\right)\leftrightarrow \left(A\in B\wedge A\in \bigcap \left\{x|\phi \right\}\right)$$
2		elintabg	$$⊢A\in B\to \left(A\in \bigcap \left\{x|\phi \right\}\leftrightarrow \forall x\left(\phi \to A\in x\right)\right)$$
3	2	pm5.32i	$$⊢\left(A\in B\wedge A\in \bigcap \left\{x|\phi \right\}\right)\leftrightarrow \left(A\in B\wedge \forall x\left(\phi \to A\in x\right)\right)$$
4	1 3	bitri	$$⊢A\in \left(B\cap \bigcap \left\{x|\phi \right\}\right)\leftrightarrow \left(A\in B\wedge \forall x\left(\phi \to A\in x\right)\right)$$