Theorem 0fv 6451

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 4119	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5542	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2870	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 315	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6441	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1653   ∈ wcel 2157  ∅c0 4115  dom cdm 5312  ‘cfv 6101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-nul 4983  ax-pow 5035

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-dm 5322  df-iota 6064  df-fv 6109

This theorem is referenced by:  fv2prc  6452  csbfv12  6455  0ov  6914  csbov123  6919  csbov  6920  elovmpt3imp  7124  bropopvvv  7492  bropfvvvvlem  7493  itunisuc  9529  itunitc1  9530  ccat1st1st  13651  str0  16236  ressbas  16255  cntrval  18064  cntzval  18066  cntzrcl  18072  sralem  19500  srasca  19504  sravsca  19505  sraip  19506  rlmval  19514  opsrle  19798  opsrbaslem  19800  mpfrcl  19840  evlval  19846  psr1val  19878  vr1val  19884  chrval  20195  ocvval  20336  elocv  20337  iscnp2  21372  resvsca  30346  mrsubfval  31922  msubfval  31938  poimirlem28  33926  0cnv  40718