Theorem 0ov 7389

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

Assertion

Ref	Expression
0ov	⊢ (𝐴∅𝐵) = ∅

Proof of Theorem 0ov

Step	Hyp	Ref	Expression
1		df-ov 7355	. 2 ⊢ (𝐴∅𝐵) = (∅‘⟨𝐴, 𝐵⟩)
2		0fv 6869	. 2 ⊢ (∅‘⟨𝐴, 𝐵⟩) = ∅
3	1, 2	eqtri 2756	1 ⊢ (𝐴∅𝐵) = ∅

Syntax hints:   = wceq 1541  ∅c0 4282  ⟨cop 4581  ‘cfv 6486  (class class class)co 7352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-dm 5629  df-iota 6442  df-fv 6494  df-ov 7355

This theorem is referenced by:  csbov  7397  2mpo0  7601  el2mpocsbcl  8021  homarcl  17937  oppglsm  19556  iswwlksnon  29833  iswspthsnon  29836  mclsrcl  35626  oppcup3  49334  indthinc  49587  indthincALT  49588  prsthinc  49589  lanrcl  49746  ranrcl  49747  rellan  49748  relran  49749