Theorem inex2g

Description: Sufficient condition for an intersection to be a set. Commuted form of inex1g . (Contributed by Peter Mazsa, 19-Dec-2018)

	Ref	Expression
Assertion	inex2g	$$⊢A\in V\to B\cap A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		incom	$$⊢B\cap A=A\cap B$$
2		inex1g	$$⊢A\in V\to A\cap B\in \mathrm{V}$$
3	1 2	eqeltrid	$$⊢A\in V\to B\cap A\in \mathrm{V}$$