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

Theorem elfvdm 5897
Description: If a function value has a member, the argument belongs to the domain. (Contributed by NM, 12-Feb-2007.)
Assertion
Ref Expression
elfvdm

Proof of Theorem elfvdm
StepHypRef Expression
1 ne0i 3790 . 2
2 ndmfv 5895 . . 3
32necon1ai 2688 . 2
41, 3syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  =/=wne 2652   c0 3784  domcdm 5004  `cfv 5593
This theorem is referenced by:  elfvex  5898  fveqdmss  6026  eldmrexrnb  6038  elmpt2cl  6517  elovmpt3rab1  6536  mpt2xopn0yelv  6960  mpt2xopxnop0  6962  r1pwss  8223  rankwflemb  8232  r1elwf  8235  rankr1ai  8237  rankdmr1  8240  rankr1ag  8241  rankr1c  8260  r1pwcl  8286  cardne  8367  cardsdomelir  8375  r1wunlim  9136  eluzel2  11115  bitsval  14074  acsfiel  15051  subcrcl  15185  homarcl2  15362  arwrcl  15371  pleval2i  15594  acsdrscl  15800  acsficl  15801  submrcl  15977  gsumws1  16007  issubg  16201  isnsg  16230  cntzrcl  16365  eldprd  17035  eldprdOLD  17037  isunit  17306  isirred  17348  issubrg  17429  abvrcl  17470  lbsss  17723  lbssp  17725  lbsind  17726  ply1frcl  18355  elocv  18699  cssi  18715  isobs  18751  linds1  18845  linds2  18846  lindsind  18852  eltg4i  19461  eltg3  19463  tg1  19465  tg2  19466  cldrcl  19527  neiss2  19602  lmrcl  19732  iscnp2  19740  islocfin  20018  kgeni  20038  kqtop  20246  elmptrab  20328  fbasne0  20331  0nelfb  20332  fbsspw  20333  fbasssin  20337  fbun  20341  trfbas2  20344  trfbas  20345  isfil  20348  filss  20354  fbasweak  20366  fgval  20371  elfg  20372  fgcl  20379  isufil  20404  ufilss  20406  trufil  20411  fmval  20444  elfm3  20451  fmfnfmlem4  20458  fmfnfm  20459  elrnust  20727  metflem  20831  xmetf  20832  xmeteq0  20841  xmettri2  20843  xmetres2  20864  blfvalps  20886  blvalps  20888  blval  20889  blfps  20909  blf  20910  isxms2  20951  tmslem  20985  metuvalOLD  21052  metuval  21053  isphtpc  21494  lmmbr2  21698  lmmbrf  21701  cfili  21707  fmcfil  21711  cfilfcls  21713  iscau2  21716  iscauf  21719  caucfil  21722  cmetcaulem  21727  iscmet3  21732  cfilresi  21734  caussi  21736  causs  21737  metcld2  21745  cmetss  21753  bcthlem1  21763  bcth3  21770  cpncn  22339  cpnres  22340  plybss  22591  tglngne  23937  2trllemF  24551  constr1trl  24590  issubgo  25305  elunirn2  27489  fpwrelmap  27556  metidval  27869  pstmval  27874  brsiga  28154  measbase  28168  cvmsrcl  28709  snmlval  28776  fneuni  30165  caures  30253  ismtyval  30296  isismty  30297  heiborlem10  30316  eldiophb  30690  elmnc  31085  issdrg  31146  submgmrcl  32470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-nul 4581  ax-pow 4630
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-dm 5014  df-iota 5556  df-fv 5601
  Copyright terms: Public domain W3C validator