Theorem 0fv 6891

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 4295	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5881	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2824	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 322	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6882	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2106  ∅c0 4287  dom cdm 5638  ‘cfv 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-dm 5648  df-iota 6453  df-fv 6509

This theorem is referenced by:  fv2prc  6892  csbfv12  6895  0ov  7399  csbov123  7404  csbov  7405  elovmpt3imp  7615  bropopvvv  8027  bropfvvvvlem  8028  itunisuc  10364  ccat1st1st  14528  str0  17072  ressbasOLD  17130  cntrval  19113  cntzval  19115  cntzrcl  19121  rlmval  20719  chrval  20965  ocvval  21108  elocv  21109  opsrle  21485  opsrbaslem  21487  opsrbaslemOLD  21488  mpfrcl  21532  evlval  21542  psr1val  21594  vr1val  21600  iscnp2  22627  resvsca  32192  mrsubfval  34189  msubfval  34205  poimirlem28  36179  0cnv  44103  elfvne0  47035