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

Theorem elfvdm 5570
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 3474 . 2  |-  ( A  e.  ( F `  B )  ->  ( F `  B )  =/=  (/) )
2 ndmfv 5568 . . 3  |-  ( -.  B  e.  dom  F  ->  ( F `  B
)  =  (/) )
32necon1ai 2501 . 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 1696    =/= wne 2459   (/)c0 3468   dom cdm 4705   ` cfv 5271
This theorem is referenced by:  elfvex  5571  elmpt2cl  6077  r1pwss  7472  rankwflemb  7481  r1elwf  7484  rankr1ai  7486  rankdmr1  7489  rankr1ag  7490  rankr1c  7509  r1pwcl  7535  cardne  7614  cardsdomelir  7622  r1wunlim  8375  eluzel2  10251  bitsval  12631  acsfiel  13572  subcrcl  13709  homarcl2  13883  arwrcl  13892  pleval2i  14114  acsdrscl  14289  acsficl  14290  submrcl  14440  gsumws1  14478  issubg  14637  isnsg  14662  cntzrcl  14819  eldprd  15255  isunit  15455  isirred  15497  issubrg  15561  abvrcl  15602  lbsss  15846  lbssp  15848  lbsind  15849  elocv  16584  cssi  16600  isobs  16636  eltg4i  16714  eltg3  16716  tg1  16718  tg2  16719  cldrcl  16779  neiss2  16854  lmrcl  16977  iscnp2  16985  kgeni  17248  kqtop  17452  elmptrab  17538  fbasne0  17541  0nelfb  17542  fbsspw  17543  fbasssin  17547  fbun  17551  trfbas2  17554  trfbas  17555  isfil  17558  filss  17564  fbasweak  17576  fgval  17581  elfg  17582  fgcl  17589  isufil  17614  ufilss  17616  trufil  17621  fmval  17654  elfm3  17661  fmfnfmlem4  17668  fmfnfm  17669  metflem  17909  xmetf  17910  xmeteq0  17919  xmettri2  17921  xmetres2  17941  blfval  17963  blval  17964  blf  17977  isxms2  18010  tmslem  18044  comet  18075  isphtpc  18508  lmmbr2  18701  lmmbrf  18704  cfili  18710  fmcfil  18714  cfilfcls  18716  iscau2  18719  iscauf  18722  caucfil  18725  cmetcaulem  18730  iscmet3  18735  cfilresi  18737  caussi  18739  causs  18740  metcld2  18748  cmetss  18756  bcthlem1  18762  bcth3  18769  cpncn  19301  cpnres  19302  plybss  19592  issubgo  20986  elunirn2  23230  brsiga  23529  measbase  23543  cvmsrcl  23810  snmlval  23929  besubbeca  25951  fneuni  26379  islocfin  26399  caures  26579  ismtyval  26627  isismty  26628  heiborlem10  26647  mzpcl34  26912  eldiophb  26939  linds1  27383  linds2  27384  lindsind  27390  elmnc  27444  issdrg  27608  mpt2xopn0yelv  28195  mpt2xopxnop0  28197  nbgrael  28275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165  ax-pow 4204
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-dm 4715  df-iota 5235  df-fv 5279
  Copyright terms: Public domain W3C validator