Theorem 0fv 6931

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ∈ wcel 2144  ∅c0 4277  dom cdm 5651  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-dm 5661  df-iota 6497  df-fv 6551

This theorem is used by:  fv2prc  6932  csbfv12  6935  0ov  7461  elfvov1  7466  elfvov2  7467  csbov123  7468  csbov  7469  elovmpt3imp  7682  bropopvvv  8106  bropfvvvvlem  8107  itunisuc  10504  ccat1st1st  14784  str0  17376  cntrval  19542  cntzval  19544  cntzrcl  19550  rlmval  21475  chrval  21838  ocvval  21982  elocv  21983  opsrle  22365  opsrbaslem  22367  mpfrcl  22403  evlval  22418  psr1val  22513  vr1val  22519  iscnp2  23566  resvsca  33943  constrext2chnlem  34432  mrsubfval  36391  msubfval  36407  poimirlem28  38703  0cnv  46888  elfvne0  50096  prcof1  50659