Theorem 0ov 7447

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 7413	. 2 ⊢ (𝐴∅𝐵) = (∅‘⟨𝐴, 𝐵⟩)
2		0fv 6925	. 2 ⊢ (∅‘⟨𝐴, 𝐵⟩) = ∅
3	1, 2	eqtri 2759	1 ⊢ (𝐴∅𝐵) = ∅

Syntax hints:   = wceq 1540  ∅c0 4313  ⟨cop 4612  ‘cfv 6536  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-dm 5669  df-iota 6489  df-fv 6544  df-ov 7413

This theorem is referenced by:  csbov  7455  2mpo0  7661  el2mpocsbcl  8089  homarcl  18046  oppglsm  19628  iswwlksnon  29840  iswspthsnon  29843  mclsrcl  35588  oppcup3  49109  indthinc  49315  indthincALT  49316  prsthinc  49317  lanrcl  49463  ranrcl  49464  rellan  49465  relran  49466