Theorem inex2

Description: Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994)

	Ref	Expression
Hypothesis	inex2.1	$$⊢A\in \mathrm{V}$$
Assertion	inex2	$$⊢B\cap A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		inex2.1	$$⊢A\in \mathrm{V}$$
2		incom	$$⊢B\cap A=A\cap B$$
3	1	inex1	$$⊢A\cap B\in \mathrm{V}$$
4	2 3	eqeltri	$$⊢B\cap A\in \mathrm{V}$$