Metamath Proof Explorer

Theorem 0ov

Description: Operation value of the empty set. (Contributed by AV, 15-May-2021)

Ref Expression
Assertion 0ov 
|- ( A (/) B ) = (/)

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( A (/) B ) = ( (/) ` <. A , B >. )
2 0fv 
 |-  ( (/) ` <. A , B >. ) = (/)
3 1 2 eqtri 
 |-  ( A (/) B ) = (/)