Theorem elfvdm 5824

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 3750	. 2 |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) )
2		ndmfv 5822	. . 3 |- ( -. B e. dom F -> ( F ` B ) = (/) )
3	2	necon1ai 2682	. 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 1758   =/= wne 2647   (/)c0 3744   dom cdm 4947   ` cfv 5525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4528  ax-pow 4577

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-dm 4957  df-iota 5488  df-fv 5533

This theorem is referenced by:  elfvex  5825  eldmrexrnb  5958  elmpt2cl  6413  mpt2xopn0yelv  6839  mpt2xopxnop0  6841  r1pwss  8101  rankwflemb  8110  r1elwf  8113  rankr1ai  8115  rankdmr1  8118  rankr1ag  8119  rankr1c  8138  r1pwcl  8164  cardne  8245  cardsdomelir  8253  r1wunlim  9014  eluzel2  10976  bitsval  13737  acsfiel  14710  subcrcl  14847  homarcl2  15021  arwrcl  15030  pleval2i  15252  acsdrscl  15458  acsficl  15459  submrcl  15592  gsumws1  15635  issubg  15799  isnsg  15828  cntzrcl  15963  eldprd  16607  eldprdOLD  16609  isunit  16871  isirred  16913  issubrg  16987  abvrcl  17028  lbsss  17280  lbssp  17282  lbsind  17283  ply1frcl  17877  elocv  18217  cssi  18233  isobs  18269  linds1  18363  linds2  18364  lindsind  18370  eltg4i  18696  eltg3  18698  tg1  18700  tg2  18701  cldrcl  18761  neiss2  18836  lmrcl  18966  iscnp2  18974  kgeni  19241  kqtop  19449  elmptrab  19531  fbasne0  19534  0nelfb  19535  fbsspw  19536  fbasssin  19540  fbun  19544  trfbas2  19547  trfbas  19548  isfil  19551  filss  19557  fbasweak  19569  fgval  19574  elfg  19575  fgcl  19582  isufil  19607  ufilss  19609  trufil  19614  fmval  19647  elfm3  19654  fmfnfmlem4  19661  fmfnfm  19662  elrnust  19930  metflem  20034  xmetf  20035  xmeteq0  20044  xmettri2  20046  xmetres2  20067  blfvalps  20089  blvalps  20091  blval  20092  blfps  20112  blf  20113  isxms2  20154  tmslem  20188  metuvalOLD  20255  metuval  20256  isphtpc  20697  lmmbr2  20901  lmmbrf  20904  cfili  20910  fmcfil  20914  cfilfcls  20916  iscau2  20919  iscauf  20922  caucfil  20925  cmetcaulem  20930  iscmet3  20935  cfilresi  20937  caussi  20939  causs  20940  metcld2  20948  cmetss  20956  bcthlem1  20966  bcth3  20973  cpncn  21542  cpnres  21543  plybss  21794  tglngne  23119  2trllemF  23599  constr1trl  23638  issubgo  23941  elunirn2  26116  fpwrelmap  26183  metidval  26461  pstmval  26466  brsiga  26741  measbase  26755  cvmsrcl  27296  snmlval  27363  fneuni  28695  islocfin  28715  caures  28803  ismtyval  28846  isismty  28847  heiborlem10  28866  eldiophb  29242  elmnc  29640  issdrg  29701  elovmpt3rab1  30310