Theorem 0fv 6926

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 4284	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5902	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2853	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 326	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6917	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  ∅c0 4279  dom cdm 5651  ‘cfv 6538

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 6494  df-fv 6546

This theorem is used by:  fv2prc  6927  csbfv12  6930  0ov  7457  elfvov1  7462  elfvov2  7463  csbov123  7464  csbov  7465  elovmpt3imp  7678  bropopvvv  8101  bropfvvvvlem  8102  itunisuc  10497  ccat1st1st  14776  str0  17367  cntrval  19533  cntzval  19535  cntzrcl  19541  rlmval  21466  chrval  21829  ocvval  21973  elocv  21974  opsrle  22356  opsrbaslem  22358  mpfrcl  22394  evlval  22409  psr1val  22504  vr1val  22510  iscnp2  23557  resvsca  33893  constrext2chnlem  34382  mrsubfval  36273  msubfval  36289  poimirlem28  38566  0cnv  46751  elfvne0  49958  prcof1  50495