Theorem 0fv 6883

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  ∅c0 4287  dom cdm 5632  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5642  df-iota 6456  df-fv 6508

This theorem is referenced by:  fv2prc  6884  csbfv12  6887  0ov  7405  elfvov1  7410  elfvov2  7411  csbov123  7412  csbov  7413  elovmpt3imp  7625  bropopvvv  8042  bropfvvvvlem  8043  itunisuc  10341  ccat1st1st  14564  str0  17128  cntrval  19260  cntzval  19262  cntzrcl  19268  rlmval  21155  chrval  21490  ocvval  21634  elocv  21635  opsrle  22014  opsrbaslem  22016  mpfrcl  22052  evlval  22067  psr1val  22138  vr1val  22144  iscnp2  23195  resvsca  33425  constrext2chnlem  33928  mrsubfval  35724  msubfval  35740  poimirlem28  37899  0cnv  46100  elfvne0  49208  prcof1  49747