Theorem 0fv 6923

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

Syntax hints:  ¬ wn 3   = wceq 1567   ∈ wcel 2149  ∅c0 4294  dom cdm 5662  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-dm 5672  df-iota 6493  df-fv 6545

This theorem is referenced by:  fv2prc  6924  csbfv12  6927  0ov  7448  elfvov1  7453  elfvov2  7454  csbov123  7455  csbov  7456  elovmpt3imp  7668  bropopvvv  8085  bropfvvvvlem  8086  itunisuc  10403  ccat1st1st  14666  str0  17249  cntrval  19389  cntzval  19391  cntzrcl  19397  rlmval  21290  chrval  21642  ocvval  21786  elocv  21787  opsrle  22167  opsrbaslem  22169  mpfrcl  22205  evlval  22220  psr1val  22315  vr1val  22321  iscnp2  23365  resvsca  33595  constrext2chnlem  34085  mrsubfval  35899  msubfval  35915  poimirlem28  38187  0cnv  46348  elfvne0  49512  prcof1  50051