Metamath Proof Explorer

Theorem inex1g

Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995)

Ref Expression
Assertion inex1g 
|- ( A e. V -> ( A i^i B ) e. _V )

Proof

Step Hyp Ref Expression
1 ineq1 
 |-  ( x = A -> ( x i^i B ) = ( A i^i B ) )
2 1 eleq1d 
 |-  ( x = A -> ( ( x i^i B ) e. _V <-> ( A i^i B ) e. _V ) )
3 vex 
 |-  x e. _V
4 3 inex1 
 |-  ( x i^i B ) e. _V
5 2 4 vtoclg 
 |-  ( A e. V -> ( A i^i B ) e. _V )