Theorem elfvdm 5898

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 3799	. 2 |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) )
2		ndmfv 5896	. . 3 |- ( -. B e. dom F -> ( F ` B ) = (/) )
3	2	necon1ai 2688	. 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 1819   =/= wne 2652   (/)c0 3793   dom cdm 5008   ` cfv 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-nul 4586  ax-pow 4634

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-dm 5018  df-iota 5557  df-fv 5602

This theorem is referenced by:  elfvex  5899  fveqdmss  6027  eldmrexrnb  6039  elmpt2cl  6516  elovmpt3rab1  6535  mpt2xopn0yelv  6959  mpt2xopxnop0  6961  r1pwss  8219  rankwflemb  8228  r1elwf  8231  rankr1ai  8233  rankdmr1  8236  rankr1ag  8237  rankr1c  8256  r1pwcl  8282  cardne  8363  cardsdomelir  8371  r1wunlim  9132  eluzel2  11111  bitsval  14086  acsfiel  15071  subcrcl  15232  homarcl2  15441  arwrcl  15450  pleval2i  15721  acsdrscl  15927  acsficl  15928  submrcl  16104  gsumws1  16134  issubg  16328  isnsg  16357  cntzrcl  16492  eldprd  17162  eldprdOLD  17164  isunit  17433  isirred  17475  issubrg  17556  abvrcl  17597  lbsss  17850  lbssp  17852  lbsind  17853  ply1frcl  18482  elocv  18826  cssi  18842  isobs  18878  linds1  18972  linds2  18973  lindsind  18979  eltg4i  19588  eltg3  19590  tg1  19592  tg2  19593  cldrcl  19654  neiss2  19729  lmrcl  19859  iscnp2  19867  islocfin  20144  kgeni  20164  kqtop  20372  elmptrab  20454  fbasne0  20457  0nelfb  20458  fbsspw  20459  fbasssin  20463  fbun  20467  trfbas2  20470  trfbas  20471  isfil  20474  filss  20480  fbasweak  20492  fgval  20497  elfg  20498  fgcl  20505  isufil  20530  ufilss  20532  trufil  20537  fmval  20570  elfm3  20577  fmfnfmlem4  20584  fmfnfm  20585  elrnust  20853  metflem  20957  xmetf  20958  xmeteq0  20967  xmettri2  20969  xmetres2  20990  blfvalps  21012  blvalps  21014  blval  21015  blfps  21035  blf  21036  isxms2  21077  tmslem  21111  metuvalOLD  21178  metuval  21179  isphtpc  21620  lmmbr2  21824  lmmbrf  21827  cfili  21833  fmcfil  21837  cfilfcls  21839  iscau2  21842  iscauf  21845  caucfil  21848  cmetcaulem  21853  iscmet3  21858  cfilresi  21860  caussi  21862  causs  21863  metcld2  21871  cmetss  21879  bcthlem1  21889  bcth3  21896  cpncn  22465  cpnres  22466  plybss  22717  tglngne  24063  2trllemF  24678  constr1trl  24717  issubgo  25432  elunirn2  27637  fpwrelmap  27713  metidval  28030  pstmval  28035  brsiga  28327  measbase  28341  cvmsrcl  28906  snmlval  28973  fneuni  30370  caures  30458  ismtyval  30501  isismty  30502  heiborlem10  30521  eldiophb  30895  elmnc  31289  issdrg  31350  submgmrcl  32732