Theorem inex2

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

	Ref	Expression
Hypothesis	inex2.1	⊢ 𝐴 ∈ V
Assertion	inex2	⊢ ( 𝐵 ∩ 𝐴 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		inex2.1	⊢ 𝐴 ∈ V
2		incom	⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 )
3	1	inex1	⊢ ( 𝐴 ∩ 𝐵 ) ∈ V
4	2 3	eqeltri	⊢ ( 𝐵 ∩ 𝐴 ) ∈ V