Theorem 0fv 6908

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 4290	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5896	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2854	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 325	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6899	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1560   ∈ wcel 2142  ∅c0 4285  dom cdm 5647  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5657  df-iota 6477  df-fv 6529

This theorem is referenced by:  fv2prc  6909  csbfv12  6912  0ov  7433  elfvov1  7438  elfvov2  7439  csbov123  7440  csbov  7441  elovmpt3imp  7653  bropopvvv  8069  bropfvvvvlem  8070  itunisuc  10376  ccat1st1st  14642  str0  17225  cntrval  19359  cntzval  19361  cntzrcl  19367  rlmval  21258  chrval  21575  ocvval  21719  elocv  21720  opsrle  22100  opsrbaslem  22102  mpfrcl  22138  evlval  22153  psr1val  22248  vr1val  22254  iscnp2  23299  resvsca  33518  constrext2chnlem  34047  mrsubfval  35858  msubfval  35874  poimirlem28  38147  0cnv  46316  elfvne0  49470  prcof1  50009