Theorem elfvdm 5711

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 3638	. 2 |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) )
2		ndmfv 5709	. . 3 |- ( -. B e. dom F -> ( F ` B ) = (/) )
3	2	necon1ai 2648	. 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 1756   =/= wne 2601   (/)c0 3632   dom cdm 4835   ` cfv 5413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416  ax-pow 4465

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-dm 4845  df-iota 5376  df-fv 5421

This theorem is referenced by:  elfvex  5712  eldmrexrnb  5845  elmpt2cl  6299  mpt2xopn0yelv  6725  mpt2xopxnop0  6727  r1pwss  7983  rankwflemb  7992  r1elwf  7995  rankr1ai  7997  rankdmr1  8000  rankr1ag  8001  rankr1c  8020  r1pwcl  8046  cardne  8127  cardsdomelir  8135  r1wunlim  8896  eluzel2  10858  bitsval  13612  acsfiel  14584  subcrcl  14721  homarcl2  14895  arwrcl  14904  pleval2i  15126  acsdrscl  15332  acsficl  15333  submrcl  15465  gsumws1  15508  issubg  15672  isnsg  15701  cntzrcl  15836  eldprd  16476  eldprdOLD  16478  isunit  16739  isirred  16781  issubrg  16845  abvrcl  16886  lbsss  17138  lbssp  17140  lbsind  17141  ply1frcl  17733  elocv  18073  cssi  18089  isobs  18125  linds1  18219  linds2  18220  lindsind  18226  eltg4i  18545  eltg3  18547  tg1  18549  tg2  18550  cldrcl  18610  neiss2  18685  lmrcl  18815  iscnp2  18823  kgeni  19090  kqtop  19298  elmptrab  19380  fbasne0  19383  0nelfb  19384  fbsspw  19385  fbasssin  19389  fbun  19393  trfbas2  19396  trfbas  19397  isfil  19400  filss  19406  fbasweak  19418  fgval  19423  elfg  19424  fgcl  19431  isufil  19456  ufilss  19458  trufil  19463  fmval  19496  elfm3  19503  fmfnfmlem4  19510  fmfnfm  19511  elrnust  19779  metflem  19883  xmetf  19884  xmeteq0  19893  xmettri2  19895  xmetres2  19916  blfvalps  19938  blvalps  19940  blval  19941  blfps  19961  blf  19962  isxms2  20003  tmslem  20037  metuvalOLD  20104  metuval  20105  isphtpc  20546  lmmbr2  20750  lmmbrf  20753  cfili  20759  fmcfil  20763  cfilfcls  20765  iscau2  20768  iscauf  20771  caucfil  20774  cmetcaulem  20779  iscmet3  20784  cfilresi  20786  caussi  20788  causs  20789  metcld2  20797  cmetss  20805  bcthlem1  20815  bcth3  20822  cpncn  21390  cpnres  21391  plybss  21642  tglngne  22964  2trllemF  23416  constr1trl  23455  issubgo  23758  elunirn2  25934  fpwrelmap  26001  metidval  26286  pstmval  26291  brsiga  26566  measbase  26580  cvmsrcl  27122  snmlval  27189  fneuni  28519  islocfin  28539  caures  28627  ismtyval  28670  isismty  28671  heiborlem10  28690  eldiophb  29066  elmnc  29464  issdrg  29525  elovmpt3rab1  30134