Theorem 0fv 6864

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  ∅c0 4284  dom cdm 5619  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-dm 5629  df-iota 6438  df-fv 6490

This theorem is referenced by:  fv2prc  6865  csbfv12  6868  0ov  7386  elfvov1  7391  elfvov2  7392  csbov123  7393  csbov  7394  elovmpt3imp  7606  bropopvvv  8023  bropfvvvvlem  8024  itunisuc  10313  ccat1st1st  14535  str0  17100  cntrval  19198  cntzval  19200  cntzrcl  19206  rlmval  21095  chrval  21430  ocvval  21574  elocv  21575  opsrle  21952  opsrbaslem  21954  mpfrcl  21990  evlval  22000  psr1val  22068  vr1val  22074  iscnp2  23124  resvsca  33270  constrext2chnlem  33717  mrsubfval  35481  msubfval  35497  poimirlem28  37628  0cnv  45723  elfvne0  48833  prcof1  49373