Theorem 0fv 6902

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

Syntax hints:  ¬ wn 3   = wceq 1540   ∈ wcel 2109  ∅c0 4296  dom cdm 5638  ‘cfv 6511

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 5261  ax-pr 5387

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519

This theorem is referenced by:  fv2prc  6903  csbfv12  6906  0ov  7424  elfvov1  7429  elfvov2  7430  csbov123  7431  csbov  7432  elovmpt3imp  7646  bropopvvv  8069  bropfvvvvlem  8070  itunisuc  10372  ccat1st1st  14593  str0  17159  cntrval  19251  cntzval  19253  cntzrcl  19259  rlmval  21098  chrval  21433  ocvval  21576  elocv  21577  opsrle  21954  opsrbaslem  21956  mpfrcl  21992  evlval  22002  psr1val  22070  vr1val  22076  iscnp2  23126  resvsca  33304  constrext2chnlem  33740  mrsubfval  35495  msubfval  35511  poimirlem28  37642  0cnv  45740  elfvne0  48837  prcof1  49377