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 incom 
 |-  ( (/) i^i A ) = ( A i^i (/) )
2 in0 
 |-  ( A i^i (/) ) = (/)
3 1 2 eqtri 
 |-  ( (/) i^i A ) = (/)