Theorem 0fv 6926

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 4291	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5912	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2857	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 326	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6917	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2146  ∅c0 4286  dom cdm 5663  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548

This theorem is used by:  fv2prc  6927  csbfv12  6930  0ov  7456  elfvov1  7461  elfvov2  7462  csbov123  7463  csbov  7464  elovmpt3imp  7677  bropopvvv  8091  bropfvvvvlem  8092  itunisuc  10418  ccat1st1st  14688  str0  17273  cntrval  19435  cntzval  19437  cntzrcl  19443  rlmval  21364  chrval  21725  ocvval  21869  elocv  21870  opsrle  22250  opsrbaslem  22252  mpfrcl  22288  evlval  22303  psr1val  22398  vr1val  22404  iscnp2  23448  resvsca  33718  constrext2chnlem  34206  mrsubfval  36039  msubfval  36055  poimirlem28  38358  0cnv  46516  elfvne0  49686  prcof1  50225