Theorem 0ov

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

	Ref	Expression
Assertion	0ov	$$⊢A\varnothing B=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$$⊢A\varnothing B=\varnothing \left(⟨A,B⟩\right)$$
2		0fv	$$⊢\varnothing \left(⟨A,B⟩\right)=\varnothing$$
3	1 2	eqtri	$$⊢A\varnothing B=\varnothing$$