Metamath Proof Explorer

Theorem inex3

Description: Sufficient condition for the intersection relation to be a set. (Contributed by Peter Mazsa, 24-Nov-2019)

Ref Expression
Assertion inex3 
|- ( ( A e. V \/ B e. W ) -> ( A i^i B ) e. _V )

Proof

Step Hyp Ref Expression
1 inex1g 
 |-  ( A e. V -> ( A i^i B ) e. _V )
2 inex2g 
 |-  ( B e. W -> ( A i^i B ) e. _V )
3 1 2 jaoi 
 |-  ( ( A e. V \/ B e. W ) -> ( A i^i B ) e. _V )