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

Theorem elfvdm 5907
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 3773 . 2  |-  ( A  e.  ( F `  B )  ->  ( F `  B )  =/=  (/) )
2 ndmfv 5905 . . 3  |-  ( -.  B  e.  dom  F  ->  ( F `  B
)  =  (/) )
32necon1ai 2662 . 2  |-  ( ( F `  B )  =/=  (/)  ->  B  e.  dom  F )
41, 3syl 17 1  |-  ( A  e.  ( F `  B )  ->  B  e.  dom  F )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870    =/= wne 2625   (/)c0 3767   dom cdm 4854   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-nul 4556  ax-pow 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-dm 4864  df-iota 5565  df-fv 5609
This theorem is referenced by:  elfvex  5908  fveqdmss  6032  eldmrexrnb  6044  elmpt2cl  6525  elovmpt3rab1  6541  mpt2xopn0yelv  6967  mpt2xopxnop0  6969  r1pwss  8254  rankwflemb  8263  r1elwf  8266  rankr1ai  8268  rankdmr1  8271  rankr1ag  8272  rankr1c  8291  r1pwcl  8317  cardne  8398  cardsdomelir  8406  r1wunlim  9161  eluzel2  11164  bitsval  14372  acsfiel  15511  subcrcl  15672  homarcl2  15881  arwrcl  15890  pleval2i  16161  acsdrscl  16367  acsficl  16368  submrcl  16544  gsumws1  16574  issubg  16768  isnsg  16797  cntzrcl  16932  eldprd  17571  isunit  17820  isirred  17862  issubrg  17943  abvrcl  17984  lbsss  18235  lbssp  18237  lbsind  18238  ply1frcl  18842  elocv  19162  cssi  19178  isobs  19214  linds1  19299  linds2  19300  lindsind  19306  eltg4i  19906  eltg3  19908  tg1  19910  tg2  19911  cldrcl  19972  neiss2  20048  lmrcl  20178  iscnp2  20186  islocfin  20463  kgeni  20483  kqtop  20691  elmptrab  20773  fbasne0  20776  0nelfb  20777  fbsspw  20778  fbasssin  20782  fbun  20786  trfbas2  20789  trfbas  20790  isfil  20793  filss  20799  fbasweak  20811  fgval  20816  elfg  20817  fgcl  20824  isufil  20849  ufilss  20851  trufil  20856  fmval  20889  elfm3  20896  fmfnfmlem4  20903  fmfnfm  20904  elrnust  21170  metflem  21274  xmetf  21275  xmeteq0  21284  xmettri2  21286  xmetres2  21307  blfvalps  21329  blvalps  21331  blval  21332  blfps  21352  blf  21353  isxms2  21394  tmslem  21428  metuval  21495  isphtpc  21918  lmmbr2  22122  lmmbrf  22125  cfili  22131  fmcfil  22135  cfilfcls  22137  iscau2  22140  iscauf  22143  caucfil  22146  cmetcaulem  22151  iscmet3  22156  cfilresi  22158  caussi  22160  causs  22161  metcld2  22169  cmetss  22177  bcthlem1  22185  bcth3  22192  cpncn  22767  cpnres  22768  plybss  23016  tglngne  24455  2trllemF  25124  constr1trl  25163  issubgo  25876  elunirn2  28090  fpwrelmap  28161  metidval  28532  pstmval  28537  brsiga  28844  measbase  28858  cvmsrcl  29775  snmlval  29842  fneuni  30788  caures  31792  ismtyval  31835  isismty  31836  heiborlem10  31855  eldiophb  35307  elmnc  35700  issdrg  35761  submgmrcl  38539  elbigofrcl  39121
  Copyright terms: Public domain W3C validator