Theorem elfvdm 5716

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 3594	. 2 |- ( A e. ( F ` B ) -> ( F ` B ) =/= (/) )
2		ndmfv 5714	. . 3 |- ( -. B e. dom F -> ( F ` B ) = (/) )
3	2	necon1ai 2609	. 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 1721   =/= wne 2567   (/)c0 3588   dom cdm 4837   ` cfv 5413

This theorem is referenced by:  elfvex  5717  eldmrexrnb  5836  elmpt2cl  6247  mpt2xopn0yelv  6423  mpt2xopxnop0  6425  r1pwss  7666  rankwflemb  7675  r1elwf  7678  rankr1ai  7680  rankdmr1  7683  rankr1ag  7684  rankr1c  7703  r1pwcl  7729  cardne  7808  cardsdomelir  7816  r1wunlim  8568  eluzel2  10449  bitsval  12891  acsfiel  13834  subcrcl  13971  homarcl2  14145  arwrcl  14154  pleval2i  14376  acsdrscl  14551  acsficl  14552  submrcl  14702  gsumws1  14740  issubg  14899  isnsg  14924  cntzrcl  15081  eldprd  15517  isunit  15717  isirred  15759  issubrg  15823  abvrcl  15864  lbsss  16104  lbssp  16106  lbsind  16107  elocv  16850  cssi  16866  isobs  16902  eltg4i  16980  eltg3  16982  tg1  16984  tg2  16985  cldrcl  17045  neiss2  17120  lmrcl  17249  iscnp2  17257  kgeni  17522  kqtop  17730  elmptrab  17812  fbasne0  17815  0nelfb  17816  fbsspw  17817  fbasssin  17821  fbun  17825  trfbas2  17828  trfbas  17829  isfil  17832  filss  17838  fbasweak  17850  fgval  17855  elfg  17856  fgcl  17863  isufil  17888  ufilss  17890  trufil  17895  fmval  17928  elfm3  17935  fmfnfmlem4  17942  fmfnfm  17943  elrnust  18207  metflem  18311  xmetf  18312  xmeteq0  18321  xmettri2  18323  xmetres2  18344  blfvalps  18366  blvalps  18368  blval  18369  blfps  18389  blf  18390  isxms2  18431  tmslem  18465  metuvalOLD  18532  metuval  18533  isphtpc  18972  lmmbr2  19165  lmmbrf  19168  cfili  19174  fmcfil  19178  cfilfcls  19180  iscau2  19183  iscauf  19186  caucfil  19189  cmetcaulem  19194  iscmet3  19199  cfilresi  19201  caussi  19203  causs  19204  metcld2  19212  cmetss  19220  bcthlem1  19230  bcth3  19237  cpncn  19775  cpnres  19776  plybss  20066  2trllemF  21502  constr1trl  21541  issubgo  21844  elunirn2  24016  metidval  24238  pstmval  24243  brsiga  24490  measbase  24504  cvmsrcl  24904  snmlval  24971  fneuni  26246  islocfin  26266  caures  26356  ismtyval  26399  isismty  26400  heiborlem10  26419  eldiophb  26705  linds1  27148  linds2  27149  lindsind  27155  elmnc  27209  issdrg  27373

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298  ax-pow 4337

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-dm 4847  df-iota 5377  df-fv 5421