Metamath Proof Explorer

Theorem inex2g

Description: Sufficient condition for an intersection to be a set. Commuted form of inex1g . (Contributed by Peter Mazsa, 19-Dec-2018)

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

Proof

Step Hyp Ref Expression
1 incom 
 |-  ( B i^i A ) = ( A i^i B )
2 inex1g 
 |-  ( A e. V -> ( A i^i B ) e. _V )
3 1 2 eqeltrid 
 |-  ( A e. V -> ( B i^i A ) e. _V )