Theorem 0ov 7449

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

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4279  ⟨cop 4590  ‘cfv 6531  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5661  df-iota 6487  df-fv 6539  df-ov 7415

This theorem is used by:  csbov  7457  2mpo0  7662  el2mpocsbcl  8085  homarcl  18183  oppglsm  19836  iswwlksnon  30424  iswspthsnon  30427  mclsrcl  36295  oppcup3  50261  indthinc  50514  indthincALT  50515  prsthinc  50516  lanrcl  50673  ranrcl  50674  rellan  50675  relran  50676