Theorem elfvdm 6130

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

Step	Hyp	Ref	Expression
1		ne0i 3880	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → (𝐹‘𝐵) ≠ ∅)
2		ndmfv 6128	. . 3 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅)
3	2	necon1ai 2809	. 2 ⊢ ((𝐹‘𝐵) ≠ ∅ → 𝐵 ∈ dom 𝐹)
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)

Syntax hints:   → wi 4   ∈ wcel 1977   ≠ wne 2780  ∅c0 3874  dom cdm 5038  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717  ax-pow 4769

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-dm 5048  df-iota 5768  df-fv 5812

This theorem is referenced by:  elfvex  6131  fveqdmss  6262  eldmrexrnb  6274  elmpt2cl  6774  elovmpt3rab1  6791  mpt2xeldm  7224  mpt2xopn0yelv  7226  mpt2xopxnop0  7228  r1pwss  8530  rankwflemb  8539  r1elwf  8542  rankr1ai  8544  rankdmr1  8547  rankr1ag  8548  rankr1c  8567  r1pwcl  8593  cardne  8674  cardsdomelir  8682  r1wunlim  9438  eluzel2  11568  bitsval  14984  acsfiel  16138  subcrcl  16299  homarcl2  16508  arwrcl  16517  pleval2i  16787  acsdrscl  16993  acsficl  16994  submrcl  17169  gsumws1  17199  issubg  17417  isnsg  17446  cntzrcl  17583  eldprd  18226  isunit  18480  isirred  18522  abvrcl  18644  lbsss  18898  lbssp  18900  lbsind  18901  ply1frcl  19504  elocv  19831  cssi  19847  isobs  19883  linds1  19968  linds2  19969  lindsind  19975  eltg4i  20575  eltg3  20577  tg1  20579  tg2  20580  cldrcl  20640  neiss2  20715  lmrcl  20845  iscnp2  20853  islocfin  21130  kgeni  21150  kqtop  21358  fbasne0  21444  0nelfb  21445  fbsspw  21446  fbasssin  21450  fbun  21454  trfbas2  21457  trfbas  21458  isfil  21461  filss  21467  fbasweak  21479  fgval  21484  elfg  21485  fgcl  21492  isufil  21517  ufilss  21519  trufil  21524  fmval  21557  elfm3  21564  fmfnfmlem4  21571  fmfnfm  21572  elrnust  21838  metflem  21943  xmetf  21944  xmeteq0  21953  xmettri2  21955  xmetres2  21976  blfvalps  21998  blvalps  22000  blval  22001  blfps  22021  blf  22022  isxms2  22063  tmslem  22097  metuval  22164  isphtpc  22601  lmmbr2  22865  lmmbrf  22868  cfili  22874  fmcfil  22878  cfilfcls  22880  iscau2  22883  iscauf  22886  caucfil  22889  cmetcaulem  22894  iscmet3  22899  cfilresi  22901  caussi  22903  causs  22904  metcld2  22913  cmetss  22921  bcthlem1  22929  bcth3  22936  cpncn  23505  cpnres  23506  plybss  23754  tglngne  25245  2trllemF  26079  constr1trl  26118  elunirn2  28831  fpwrelmap  28896  metidval  29261  pstmval  29266  brsiga  29573  measbase  29587  cvmsrcl  30500  snmlval  30567  fneuni  31512  uncf  32558  unccur  32562  caures  32726  ismtyval  32769  isismty  32770  heiborlem10  32789  eldiophb  36338  elmnc  36725  issdrg  36786  1wlkdlem3  40893  11wlkdlem3  41306  submgmrcl  41572  elbigofrcl  42142