Theorem 0fv 6925

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  ∅c0 4313  dom cdm 5659  ‘cfv 6536

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 2708  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-dm 5669  df-iota 6489  df-fv 6544

This theorem is referenced by:  fv2prc  6926  csbfv12  6929  0ov  7447  elfvov1  7452  elfvov2  7453  csbov123  7454  csbov  7455  elovmpt3imp  7669  bropopvvv  8094  bropfvvvvlem  8095  itunisuc  10438  ccat1st1st  14651  str0  17213  cntrval  19307  cntzval  19309  cntzrcl  19315  rlmval  21154  chrval  21489  ocvval  21632  elocv  21633  opsrle  22010  opsrbaslem  22012  mpfrcl  22048  evlval  22058  psr1val  22126  vr1val  22132  iscnp2  23182  resvsca  33353  constrext2chnlem  33789  mrsubfval  35535  msubfval  35551  poimirlem28  37677  0cnv  45738  elfvne0  48794  prcof1  49265