Theorem 0ov 7427

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

Syntax hints:   = wceq 1540  ∅c0 4299  ⟨cop 4598  ‘cfv 6514  (class class class)co 7390

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 2702  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-dm 5651  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  csbov  7435  2mpo0  7641  el2mpocsbcl  8067  homarcl  17997  oppglsm  19579  iswwlksnon  29790  iswspthsnon  29793  mclsrcl  35555  oppcup3  49202  indthinc  49455  indthincALT  49456  prsthinc  49457  lanrcl  49614  ranrcl  49615  rellan  49616  relran  49617