Theorem elintdv

Description: Membership in class intersection. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	elintdv.1	$$⊢\phi \to A\in V$$
	elintdv.2	$$⊢\left(\phi \wedge x\in B\right)\to A\in x$$
Assertion	elintdv	$$⊢\phi \to A\in \bigcap B$$

Proof

Step	Hyp	Ref	Expression
1		elintdv.1	$$⊢\phi \to A\in V$$
2		elintdv.2	$$⊢\left(\phi \wedge x\in B\right)\to A\in x$$
3		nfv	$$⊢Ⅎx\phi$$
4	3 1 2	elintd	$$⊢\phi \to A\in \bigcap B$$