Theorem 0fv 6227

Description: Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014.)

Assertion

Ref	Expression
0fv	|- ( (/) ` A ) = (/)

Proof of Theorem 0fv

Step	Hyp	Ref	Expression
1		noel 3919	. . 3 |- -. A e. (/)
2		dm0 5339	. . . 4 |- dom (/) = (/)
3	2	eleq2i 2693	. . 3 |- ( A e. dom (/) <-> A e. (/) )
4	1, 3	mtbir 313	. 2 |- -. A e. dom (/)
5		ndmfv 6218	. 2 |- ( -. A e. dom (/) -> ( (/) ` A ) = (/) )
6	4, 5	ax-mp 5	1 |- ( (/) ` A ) = (/)

Syntax hints:   -. wn 3   = wceq 1483   e. wcel 1990   (/)c0 3915   dom cdm 5114   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-dm 5124  df-iota 5851  df-fv 5896

This theorem is referenced by:  fv2prc  6228  csbfv12  6231  0ov  6682  csbov123  6687  csbov  6688  elovmpt3imp  6890  bropopvvv  7255  bropfvvvvlem  7256  itunisuc  9241  itunitc1  9242  str0  15911  ressbas  15930  cntrval  17752  cntzval  17754  cntzrcl  17760  sralem  19177  srasca  19181  sravsca  19182  sraip  19183  rlmval  19191  opsrle  19475  opsrbaslem  19477  opsrbaslemOLD  19478  mpfrcl  19518  evlval  19524  psr1val  19556  vr1val  19562  chrval  19873  ocvval  20011  elocv  20012  iscnp2  21043  resvsca  29830  mrsubfval  31405  msubfval  31421  poimirlem28  33437  0cnv  39974