Metamath Proof Explorer

Theorem 0in

Description: The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion 0in 
|- ( (/) i^i A ) = (/)

Proof

Step Hyp Ref Expression
1 in0 
 |-  ( A i^i (/) ) = (/)
2 1 ineqcomi 
 |-  ( (/) i^i A ) = (/)