Theorem 0fv 6370

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 4067	. . 3 ⊢ ¬ 𝐴 ∈ ∅
2		dm0 5476	. . . 4 ⊢ dom ∅ = ∅
3	2	eleq2i 2842	. . 3 ⊢ (𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅)
4	1, 3	mtbir 312	. 2 ⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv 6361	. 2 ⊢ (¬ 𝐴 ∈ dom ∅ → (∅‘𝐴) = ∅)
6	4, 5	ax-mp 5	1 ⊢ (∅‘𝐴) = ∅

Syntax hints:  ¬ wn 3   = wceq 1631   ∈ wcel 2145  ∅c0 4063  dom cdm 5250  ‘cfv 6030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4924  ax-pow 4975

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-dm 5260  df-iota 5993  df-fv 6038

This theorem is referenced by:  fv2prc  6371  csbfv12  6374  0ov  6831  csbov123  6836  csbov  6837  elovmpt3imp  7041  bropopvvv  7410  bropfvvvvlem  7411  itunisuc  9447  itunitc1  9448  ccat1st1st  13611  str0  16118  ressbas  16137  cntrval  17959  cntzval  17961  cntzrcl  17967  sralem  19392  srasca  19396  sravsca  19397  sraip  19398  rlmval  19406  opsrle  19690  opsrbaslem  19692  opsrbaslemOLD  19693  mpfrcl  19733  evlval  19739  psr1val  19771  vr1val  19777  chrval  20088  ocvval  20228  elocv  20229  iscnp2  21264  resvsca  30170  mrsubfval  31743  msubfval  31759  poimirlem28  33769  0cnv  40487