Theorem 0ov 7460

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

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4289  ⟨cop 4600  ‘cfv 6543  (class class class)co 7423

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-dm 5676  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  csbov  7468  2mpo0  7672  el2mpocsbcl  8089  homarcl  18110  oppglsm  19743  iswwlksnon  30239  iswspthsnon  30242  mclsrcl  36074  oppcup3  50028  indthinc  50281  indthincALT  50282  prsthinc  50283  lanrcl  50440  ranrcl  50441  rellan  50442  relran  50443