Theorem elfvdm 5905

Description: If a function value has a member, the argument belongs to the domain. (Contributed by NM, 12-Feb-2007.)

Assertion

Ref	Expression
elfvdm	|- ( A e. ( F ` B ) -> B e. dom F )

Proof of Theorem elfvdm

Step	Hyp	Ref	Expression
1		ne0i 3728	. 2 |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) )
2		ndmfv 5903	. . 3 |- ( -. B e. dom F -> ( F ` B ) = (/) )
3	2	necon1ai 2670	. 2 |- ( ( F ` B ) =/= (/) -> B e. dom F )
4	1, 3	syl 17	1 |- ( A e. ( F ` B ) -> B e. dom F )

Syntax hints:   -> wi 4   e. wcel 1904   =/= wne 2641   (/)c0 3722   dom cdm 4839   ` cfv 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-nul 4527  ax-pow 4579

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-dm 4849  df-iota 5553  df-fv 5597

This theorem is referenced by:  elfvex  5906  fveqdmss  6032  eldmrexrnb  6044  elmpt2cl  6530  elovmpt3rab1  6546  mpt2xeldm  6976  mpt2xopn0yelv  6978  mpt2xopxnop0  6980  r1pwss  8273  rankwflemb  8282  r1elwf  8285  rankr1ai  8287  rankdmr1  8290  rankr1ag  8291  rankr1c  8310  r1pwcl  8336  cardne  8417  cardsdomelir  8425  r1wunlim  9180  eluzel2  11187  bitsval  14476  acsfiel  15638  subcrcl  15799  homarcl2  16008  arwrcl  16017  pleval2i  16288  acsdrscl  16494  acsficl  16495  submrcl  16671  gsumws1  16701  issubg  16895  isnsg  16924  cntzrcl  17059  eldprd  17714  isunit  17963  isirred  18005  abvrcl  18127  lbsss  18378  lbssp  18380  lbsind  18381  ply1frcl  18984  elocv  19308  cssi  19324  isobs  19360  linds1  19445  linds2  19446  lindsind  19452  eltg4i  20052  eltg3  20054  tg1  20056  tg2  20057  cldrcl  20118  neiss2  20194  lmrcl  20324  iscnp2  20332  islocfin  20609  kgeni  20629  kqtop  20837  fbasne0  20923  0nelfb  20924  fbsspw  20925  fbasssin  20929  fbun  20933  trfbas2  20936  trfbas  20937  isfil  20940  filss  20946  fbasweak  20958  fgval  20963  elfg  20964  fgcl  20971  isufil  20996  ufilss  20998  trufil  21003  fmval  21036  elfm3  21043  fmfnfmlem4  21050  fmfnfm  21051  elrnust  21317  metflem  21421  xmetf  21422  xmeteq0  21431  xmettri2  21433  xmetres2  21454  blfvalps  21476  blvalps  21478  blval  21479  blfps  21499  blf  21500  isxms2  21541  tmslem  21575  metuval  21642  isphtpc  22103  lmmbr2  22307  lmmbrf  22310  cfili  22316  fmcfil  22320  cfilfcls  22322  iscau2  22325  iscauf  22328  caucfil  22331  cmetcaulem  22336  iscmet3  22341  cfilresi  22343  caussi  22345  causs  22346  metcld2  22354  cmetss  22362  bcthlem1  22370  bcth3  22377  cpncn  22969  cpnres  22970  plybss  23227  tglngne  24674  2trllemF  25358  constr1trl  25397  issubgo  26112  elunirn2  28326  fpwrelmap  28393  metidval  28767  pstmval  28772  brsiga  29079  measbase  29093  cvmsrcl  30059  snmlval  30126  fneuni  31074  caures  32153  ismtyval  32196  isismty  32197  heiborlem10  32216  eldiophb  35670  elmnc  36066  issdrg  36134  1wlkdlem3  39884  11wlkdlem3  40027  submgmrcl  40290  elbigofrcl  40869