MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfvdm Unicode version

Theorem elfvdm 5554
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
StepHypRef Expression
1 ne0i 3461 . 2  |-  ( A  e.  ( F `  B )  ->  ( F `  B )  =/=  (/) )
2 ndmfv 5552 . . 3  |-  ( -.  B  e.  dom  F  ->  ( F `  B
)  =  (/) )
32necon1ai 2488 . 2  |-  ( ( F `  B )  =/=  (/)  ->  B  e.  dom  F )
41, 3syl 15 1  |-  ( A  e.  ( F `  B )  ->  B  e.  dom  F )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    =/= wne 2446   (/)c0 3455   dom cdm 4689   ` cfv 5255
This theorem is referenced by:  elfvex  5555  elmpt2cl  6061  r1pwss  7456  rankwflemb  7465  r1elwf  7468  rankr1ai  7470  rankdmr1  7473  rankr1ag  7474  rankr1c  7493  r1pwcl  7519  cardne  7598  cardsdomelir  7606  r1wunlim  8359  eluzel2  10235  bitsval  12615  acsfiel  13556  subcrcl  13693  homarcl2  13867  arwrcl  13876  pleval2i  14098  acsdrscl  14273  acsficl  14274  submrcl  14424  gsumws1  14462  issubg  14621  isnsg  14646  cntzrcl  14803  eldprd  15239  isunit  15439  isirred  15481  issubrg  15545  abvrcl  15586  lbsss  15830  lbssp  15832  lbsind  15833  elocv  16568  cssi  16584  isobs  16620  eltg4i  16698  eltg3  16700  tg1  16702  tg2  16703  cldrcl  16763  neiss2  16838  lmrcl  16961  iscnp2  16969  kgeni  17232  kqtop  17436  elmptrab  17522  fbasne0  17525  0nelfb  17526  fbsspw  17527  fbasssin  17531  fbun  17535  trfbas2  17538  trfbas  17539  isfil  17542  filss  17548  fbasweak  17560  fgval  17565  elfg  17566  fgcl  17573  isufil  17598  ufilss  17600  trufil  17605  fmval  17638  elfm3  17645  fmfnfmlem4  17652  fmfnfm  17653  metflem  17893  xmetf  17894  xmeteq0  17903  xmettri2  17905  xmetres2  17925  blfval  17947  blval  17948  blf  17961  isxms2  17994  tmslem  18028  comet  18059  isphtpc  18492  lmmbr2  18685  lmmbrf  18688  cfili  18694  fmcfil  18698  cfilfcls  18700  iscau2  18703  iscauf  18706  caucfil  18709  cmetcaulem  18714  iscmet3  18719  cfilresi  18721  caussi  18723  causs  18724  metcld2  18732  cmetss  18740  bcthlem1  18746  bcth3  18753  cpncn  19285  cpnres  19286  plybss  19576  issubgo  20970  elunirn2  23215  brsiga  23514  measbase  23528  cvmsrcl  23795  snmlval  23914  besubbeca  25848  fneuni  26276  islocfin  26296  caures  26476  ismtyval  26524  isismty  26525  heiborlem10  26544  mzpcl34  26809  eldiophb  26836  linds1  27280  linds2  27281  lindsind  27287  elmnc  27341  issdrg  27505  mpt2xopn0yelv  28079  mpt2xopxnop0  28081  nbgrael  28141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149  ax-pow 4188
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-dm 4699  df-iota 5219  df-fv 5263
  Copyright terms: Public domain W3C validator