Theorem elfvdm 5851

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 3710	. 2 |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) )
2		ndmfv 5849	. . 3 |- ( -. B e. dom F -> ( F ` B ) = (/) )
3	2	necon1ai 2628	. 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 1872   =/= wne 2599   (/)c0 3704   dom cdm 4796   ` cfv 5544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-nul 4498  ax-pow 4545

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-dm 4806  df-iota 5508  df-fv 5552

This theorem is referenced by:  elfvex  5852  fveqdmss  5976  eldmrexrnb  5988  elmpt2cl  6469  elovmpt3rab1  6485  mpt2xeldm  6912  mpt2xopn0yelv  6914  mpt2xopxnop0  6916  r1pwss  8207  rankwflemb  8216  r1elwf  8219  rankr1ai  8221  rankdmr1  8224  rankr1ag  8225  rankr1c  8244  r1pwcl  8270  cardne  8351  cardsdomelir  8359  r1wunlim  9113  eluzel2  11115  bitsval  14340  acsfiel  15503  subcrcl  15664  homarcl2  15873  arwrcl  15882  pleval2i  16153  acsdrscl  16359  acsficl  16360  submrcl  16536  gsumws1  16566  issubg  16760  isnsg  16789  cntzrcl  16924  eldprd  17579  isunit  17828  isirred  17870  abvrcl  17992  lbsss  18243  lbssp  18245  lbsind  18246  ply1frcl  18850  elocv  19173  cssi  19189  isobs  19225  linds1  19310  linds2  19311  lindsind  19317  eltg4i  19917  eltg3  19919  tg1  19921  tg2  19922  cldrcl  19983  neiss2  20059  lmrcl  20189  iscnp2  20197  islocfin  20474  kgeni  20494  kqtop  20702  fbasne0  20787  0nelfb  20788  fbsspw  20789  fbasssin  20793  fbun  20797  trfbas2  20800  trfbas  20801  isfil  20804  filss  20810  fbasweak  20822  fgval  20827  elfg  20828  fgcl  20835  isufil  20860  ufilss  20862  trufil  20867  fmval  20900  elfm3  20907  fmfnfmlem4  20914  fmfnfm  20915  elrnust  21181  metflem  21285  xmetf  21286  xmeteq0  21295  xmettri2  21297  xmetres2  21318  blfvalps  21340  blvalps  21342  blval  21343  blfps  21363  blf  21364  isxms2  21405  tmslem  21439  metuval  21506  isphtpc  21967  lmmbr2  22171  lmmbrf  22174  cfili  22180  fmcfil  22184  cfilfcls  22186  iscau2  22189  iscauf  22192  caucfil  22195  cmetcaulem  22200  iscmet3  22205  cfilresi  22207  caussi  22209  causs  22210  metcld2  22218  cmetss  22226  bcthlem1  22234  bcth3  22241  cpncn  22832  cpnres  22833  plybss  23090  tglngne  24537  2trllemF  25221  constr1trl  25260  issubgo  25973  elunirn2  28196  fpwrelmap  28268  metidval  28645  pstmval  28650  brsiga  28957  measbase  28971  cvmsrcl  29939  snmlval  30006  fneuni  30952  caures  31996  ismtyval  32039  isismty  32040  heiborlem10  32059  eldiophb  35511  elmnc  35908  issdrg  35976  submgmrcl  39383  elbigofrcl  39964