Theorem 0fv 6697

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

Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2111  ∅c0 4225  dom cdm 5524  ‘cfv 6335

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-dm 5534  df-iota 6294  df-fv 6343

This theorem is referenced by:  fv2prc  6698  csbfv12  6701  0ov  7187  csbov123  7192  csbov  7193  elovmpt3imp  7398  bropopvvv  7790  bropfvvvvlem  7791  itunisuc  9879  ccat1st1st  14031  str0  16593  ressbas  16612  cntrval  18516  cntzval  18518  cntzrcl  18524  rlmval  20031  chrval  20293  ocvval  20432  elocv  20433  opsrle  20807  opsrbaslem  20809  mpfrcl  20848  evlval  20858  psr1val  20910  vr1val  20916  iscnp2  21939  resvsca  31055  mrsubfval  32986  msubfval  33002  poimirlem28  35365  0cnv  42750