Theorem 0fv 6873

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

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2113  ∅c0 4283  dom cdm 5622  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-dm 5632  df-iota 6446  df-fv 6498

This theorem is referenced by:  fv2prc  6874  csbfv12  6877  0ov  7393  elfvov1  7398  elfvov2  7399  csbov123  7400  csbov  7401  elovmpt3imp  7613  bropopvvv  8030  bropfvvvvlem  8031  itunisuc  10327  ccat1st1st  14550  str0  17114  cntrval  19246  cntzval  19248  cntzrcl  19254  rlmval  21141  chrval  21476  ocvval  21620  elocv  21621  opsrle  22000  opsrbaslem  22002  mpfrcl  22038  evlval  22053  psr1val  22124  vr1val  22130  iscnp2  23181  resvsca  33362  constrext2chnlem  33856  mrsubfval  35651  msubfval  35667  poimirlem28  37788  0cnv  45928  elfvne0  49036  prcof1  49575