Theorem 0fv 6930

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 4318	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5911	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2825	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 323	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6921	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2107  ∅c0 4313  dom cdm 5665  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-dm 5675  df-iota 6494  df-fv 6549

This theorem is referenced by:  fv2prc  6931  csbfv12  6934  0ov  7450  elfvov1  7455  elfvov2  7456  csbov123  7457  csbov  7458  elovmpt3imp  7672  bropopvvv  8097  bropfvvvvlem  8098  itunisuc  10441  ccat1st1st  14648  str0  17208  ressbasOLD  17259  cntrval  19306  cntzval  19308  cntzrcl  19314  rlmval  21160  chrval  21496  ocvval  21639  elocv  21640  opsrle  22019  opsrbaslem  22021  mpfrcl  22057  evlval  22067  psr1val  22135  vr1val  22141  iscnp2  23193  resvsca  33296  constrext2chnlem  33730  mrsubfval  35472  msubfval  35488  poimirlem28  37614  0cnv  45714  elfvne0  48716