Metamath Proof Explorer


Theorem inex2

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

Ref Expression
Hypothesis inex2.1 AV
Assertion inex2 BAV

Proof

Step Hyp Ref Expression
1 inex2.1 AV
2 incom BA=AB
3 1 inex1 ABV
4 2 3 eqeltri BAV