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

Theorem elfvdm 6447
Description: If a function value has a member, the argument belongs to the domain. (Contributed by NM, 12-Feb-2007.)
Assertion
Ref Expression
elfvdm (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)

Proof of Theorem elfvdm
StepHypRef Expression
1 ne0i 4133 . 2 (𝐴 ∈ (𝐹𝐵) → (𝐹𝐵) ≠ ∅)
2 ndmfv 6445 . . 3 𝐵 ∈ dom 𝐹 → (𝐹𝐵) = ∅)
32necon1ai 3016 . 2 ((𝐹𝐵) ≠ ∅ → 𝐵 ∈ dom 𝐹)
41, 3syl 17 1 (𝐴 ∈ (𝐹𝐵) → 𝐵 ∈ dom 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  wne 2989  c0 4127  dom cdm 5322  cfv 6108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-nul 4994  ax-pow 5046
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-dm 5332  df-iota 6071  df-fv 6116
This theorem is referenced by:  elfvex  6448  fveqdmss  6583  eldmrexrnb  6595  elmpt2cl  7113  elovmpt3rab1  7130  mpt2xeldm  7579  mpt2xopn0yelv  7581  mpt2xopxnop0  7583  r1pwss  8901  rankwflemb  8910  r1elwf  8913  rankr1ai  8915  rankdmr1  8918  rankr1ag  8919  rankr1c  8938  r1pwcl  8964  cardne  9081  cardsdomelir  9089  r1wunlim  9851  eluzel2  11916  bitsval  15372  acsfiel  16526  subcrcl  16687  homarcl2  16896  arwrcl  16905  pleval2i  17176  acsdrscl  17382  acsficl  17383  submrcl  17558  gsumws1  17588  issubg  17803  isnsg  17832  cntzrcl  17968  eldprd  18612  isunit  18866  isirred  18908  abvrcl  19032  lbsss  19291  lbssp  19293  lbsind  19294  ply1frcl  19898  elocv  20230  cssi  20246  isobs  20282  linds1  20367  linds2  20368  lindsind  20374  eltg4i  20986  eltg3  20988  tg1  20990  tg2  20991  cldrcl  21052  neiss2  21127  lmrcl  21257  iscnp2  21265  islocfin  21542  kgeni  21562  kqtop  21770  fbasne0  21855  0nelfb  21856  fbsspw  21857  fbasssin  21861  fbun  21865  trfbas2  21868  trfbas  21869  isfil  21872  filss  21878  fbasweak  21890  fgval  21895  elfg  21896  fgcl  21903  isufil  21928  ufilss  21930  trufil  21935  fmval  21968  elfm3  21975  fmfnfmlem4  21982  fmfnfm  21983  elrnust  22249  metflem  22354  xmetf  22355  xmeteq0  22364  xmettri2  22366  xmetres2  22387  blfvalps  22409  blvalps  22411  blval  22412  blfps  22432  blf  22433  isxms2  22474  tmslem  22508  metuval  22575  isphtpc  23014  lmmbr2  23278  lmmbrf  23281  cfili  23287  fmcfil  23291  cfilfcls  23293  iscau2  23296  iscauf  23299  caucfil  23302  cmetcaulem  23307  iscmet3  23312  cfilresi  23314  caussi  23316  causs  23317  metcld2  23326  cmetss  23334  bcthlem1  23342  bcth3  23349  cpncn  23923  cpnres  23924  plybss  24174  tglngne  25669  wlkdlem3  26819  1wlkdlem3  27322  elunirn2  29788  fpwrelmap  29845  metidval  30268  pstmval  30273  brsiga  30581  measbase  30595  cvmsrcl  31578  snmlval  31645  fneuni  32672  uncf  33707  unccur  33711  caures  33873  ismtyval  33916  isismty  33917  heiborlem10  33936  eldiophb  37827  elmnc  38212  issdrg  38273  submgmrcl  42355  elbigofrcl  42917
  Copyright terms: Public domain W3C validator