Theorem 0fv 6881

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

Syntax hints:  ¬ wn 3   = wceq 1542   ∈ wcel 2114  ∅c0 4273  dom cdm 5631  ‘cfv 6498

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 2708  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-dm 5641  df-iota 6454  df-fv 6506

This theorem is referenced by:  fv2prc  6882  csbfv12  6885  0ov  7404  elfvov1  7409  elfvov2  7410  csbov123  7411  csbov  7412  elovmpt3imp  7624  bropopvvv  8040  bropfvvvvlem  8041  itunisuc  10341  ccat1st1st  14591  str0  17159  cntrval  19294  cntzval  19296  cntzrcl  19302  rlmval  21186  chrval  21503  ocvval  21647  elocv  21648  opsrle  22025  opsrbaslem  22027  mpfrcl  22063  evlval  22078  psr1val  22149  vr1val  22155  iscnp2  23204  resvsca  33392  constrext2chnlem  33894  mrsubfval  35690  msubfval  35706  poimirlem28  37969  0cnv  46170  elfvne0  49324  prcof1  49863