Description: The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17Aug2020)
Ref  Expression  

Assertion  0in   ( (/) i^i A ) = (/) 
Step  Hyp  Ref  Expression 

1  incom   ( (/) i^i A ) = ( A i^i (/) ) 

2  in0   ( A i^i (/) ) = (/) 

3  1 2  eqtri   ( (/) i^i A ) = (/) 