Metamath Proof Explorer

Theorem inex2

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

Ref Expression
Hypothesis inex2.1 
|- A e. _V
Assertion inex2 
|- ( B i^i A ) e. _V

Proof

Step Hyp Ref Expression
1 inex2.1 
 |-  A e. _V
2 incom 
 |-  ( B i^i A ) = ( A i^i B )
3 1 inex1 
 |-  ( A i^i B ) e. _V
4 2 3 eqeltri 
 |-  ( B i^i A ) e. _V