Theorem 0fv 6868

Description: Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)

Assertion

Ref	Expression
0fv	⊢ (∅‘𝐴) = ∅

Proof of Theorem 0fv

Step	Hyp	Ref	Expression
1		noel 4266	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5862	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2831	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 324	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6859	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1547   ∈ wcel 2119  ∅c0 4261  dom cdm 5618  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-dm 5628  df-iota 6441  df-fv 6493

This theorem is referenced by:  fv2prc  6869  csbfv12  6872  0ov  7393  elfvov1  7398  elfvov2  7399  csbov123  7400  csbov  7401  elovmpt3imp  7613  bropopvvv  8029  bropfvvvvlem  8030  itunisuc  10332  ccat1st1st  14582  str0  17150  cntrval  19285  cntzval  19287  cntzrcl  19293  rlmval  21181  chrval  21498  ocvval  21642  elocv  21643  opsrle  22023  opsrbaslem  22025  mpfrcl  22061  evlval  22076  psr1val  22171  vr1val  22177  iscnp2  23222  resvsca  33415  constrext2chnlem  33934  mrsubfval  35736  msubfval  35752  poimirlem28  38015  0cnv  46185  elfvne0  49339  prcof1  49878