Theorem 0fv 6951

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

Syntax hints:  ¬ wn 3   = wceq 1537   ∈ wcel 2106  ∅c0 4339  dom cdm 5689  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-dm 5699  df-iota 6516  df-fv 6571

This theorem is referenced by:  fv2prc  6952  csbfv12  6955  0ov  7468  elfvov1  7473  elfvov2  7474  csbov123  7475  csbov  7476  elovmpt3imp  7690  bropopvvv  8114  bropfvvvvlem  8115  itunisuc  10457  ccat1st1st  14663  str0  17223  ressbasOLD  17281  cntrval  19350  cntzval  19352  cntzrcl  19358  rlmval  21216  chrval  21556  ocvval  21703  elocv  21704  opsrle  22083  opsrbaslem  22085  opsrbaslemOLD  22086  mpfrcl  22127  evlval  22137  psr1val  22203  vr1val  22209  iscnp2  23263  resvsca  33336  mrsubfval  35493  msubfval  35509  poimirlem28  37635  0cnv  45698  elfvne0  48679