Theorem elfvdm 5892

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 3791	. 2 |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) )
2		ndmfv 5890	. . 3 |- ( -. B e. dom F -> ( F ` B ) = (/) )
3	2	necon1ai 2698	. 2 |- ( ( F ` B ) =/= (/) -> B e. dom F )
4	1, 3	syl 16	1 |- ( A e. ( F ` B ) -> B e. dom F )

Syntax hints:   -> wi 4   e. wcel 1767   =/= wne 2662   (/)c0 3785   dom cdm 4999   ` cfv 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4576  ax-pow 4625

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-dm 5009  df-iota 5551  df-fv 5596

This theorem is referenced by:  elfvex  5893  eldmrexrnb  6028  elmpt2cl  6501  elovmpt3rab1  6520  mpt2xopn0yelv  6941  mpt2xopxnop0  6943  r1pwss  8202  rankwflemb  8211  r1elwf  8214  rankr1ai  8216  rankdmr1  8219  rankr1ag  8220  rankr1c  8239  r1pwcl  8265  cardne  8346  cardsdomelir  8354  r1wunlim  9115  eluzel2  11087  bitsval  13933  acsfiel  14909  subcrcl  15046  homarcl2  15220  arwrcl  15229  pleval2i  15451  acsdrscl  15657  acsficl  15658  submrcl  15796  gsumws1  15839  issubg  16006  isnsg  16035  cntzrcl  16170  eldprd  16838  eldprdOLD  16840  isunit  17107  isirred  17149  issubrg  17229  abvrcl  17270  lbsss  17523  lbssp  17525  lbsind  17526  ply1frcl  18154  elocv  18494  cssi  18510  isobs  18546  linds1  18640  linds2  18641  lindsind  18647  eltg4i  19256  eltg3  19258  tg1  19260  tg2  19261  cldrcl  19321  neiss2  19396  lmrcl  19526  iscnp2  19534  kgeni  19801  kqtop  20009  elmptrab  20091  fbasne0  20094  0nelfb  20095  fbsspw  20096  fbasssin  20100  fbun  20104  trfbas2  20107  trfbas  20108  isfil  20111  filss  20117  fbasweak  20129  fgval  20134  elfg  20135  fgcl  20142  isufil  20167  ufilss  20169  trufil  20174  fmval  20207  elfm3  20214  fmfnfmlem4  20221  fmfnfm  20222  elrnust  20490  metflem  20594  xmetf  20595  xmeteq0  20604  xmettri2  20606  xmetres2  20627  blfvalps  20649  blvalps  20651  blval  20652  blfps  20672  blf  20673  isxms2  20714  tmslem  20748  metuvalOLD  20815  metuval  20816  isphtpc  21257  lmmbr2  21461  lmmbrf  21464  cfili  21470  fmcfil  21474  cfilfcls  21476  iscau2  21479  iscauf  21482  caucfil  21485  cmetcaulem  21490  iscmet3  21495  cfilresi  21497  caussi  21499  causs  21500  metcld2  21508  cmetss  21516  bcthlem1  21526  bcth3  21533  cpncn  22102  cpnres  22103  plybss  22354  tglngne  23693  2trllemF  24255  constr1trl  24294  issubgo  25009  elunirn2  27189  fpwrelmap  27256  metidval  27533  pstmval  27538  brsiga  27822  measbase  27836  cvmsrcl  28377  snmlval  28444  fneuni  29776  islocfin  29796  caures  29884  ismtyval  29927  isismty  29928  heiborlem10  29947  eldiophb  30322  elmnc  30718  issdrg  30779