Theorem elfvdm 6220

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 3921	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → (𝐹‘𝐵) ≠ ∅)
2		ndmfv 6218	. . 3 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅)
3	2	necon1ai 2821	. 2 ⊢ ((𝐹‘𝐵) ≠ ∅ → 𝐵 ∈ dom 𝐹)
4	1, 3	syl 17	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)

Syntax hints:   → wi 4   ∈ wcel 1990   ≠ wne 2794  ∅c0 3915  dom cdm 5114  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789  ax-pow 4843

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-dm 5124  df-iota 5851  df-fv 5896

This theorem is referenced by:  elfvex  6221  fveqdmss  6354  eldmrexrnb  6366  elmpt2cl  6876  elovmpt3rab1  6893  mpt2xeldm  7337  mpt2xopn0yelv  7339  mpt2xopxnop0  7341  r1pwss  8647  rankwflemb  8656  r1elwf  8659  rankr1ai  8661  rankdmr1  8664  rankr1ag  8665  rankr1c  8684  r1pwcl  8710  cardne  8791  cardsdomelir  8799  r1wunlim  9559  eluzel2  11692  bitsval  15146  acsfiel  16315  subcrcl  16476  homarcl2  16685  arwrcl  16694  pleval2i  16964  acsdrscl  17170  acsficl  17171  submrcl  17346  gsumws1  17376  issubg  17594  isnsg  17623  cntzrcl  17760  eldprd  18403  isunit  18657  isirred  18699  abvrcl  18821  lbsss  19077  lbssp  19079  lbsind  19080  ply1frcl  19683  elocv  20012  cssi  20028  isobs  20064  linds1  20149  linds2  20150  lindsind  20156  eltg4i  20764  eltg3  20766  tg1  20768  tg2  20769  cldrcl  20830  neiss2  20905  lmrcl  21035  iscnp2  21043  islocfin  21320  kgeni  21340  kqtop  21548  fbasne0  21634  0nelfb  21635  fbsspw  21636  fbasssin  21640  fbun  21644  trfbas2  21647  trfbas  21648  isfil  21651  filss  21657  fbasweak  21669  fgval  21674  elfg  21675  fgcl  21682  isufil  21707  ufilss  21709  trufil  21714  fmval  21747  elfm3  21754  fmfnfmlem4  21761  fmfnfm  21762  elrnust  22028  metflem  22133  xmetf  22134  xmeteq0  22143  xmettri2  22145  xmetres2  22166  blfvalps  22188  blvalps  22190  blval  22191  blfps  22211  blf  22212  isxms2  22253  tmslem  22287  metuval  22354  isphtpc  22793  lmmbr2  23057  lmmbrf  23060  cfili  23066  fmcfil  23070  cfilfcls  23072  iscau2  23075  iscauf  23078  caucfil  23081  cmetcaulem  23086  iscmet3  23091  cfilresi  23093  caussi  23095  causs  23096  metcld2  23105  cmetss  23113  bcthlem1  23121  bcth3  23128  cpncn  23699  cpnres  23700  plybss  23950  tglngne  25445  wlkdlem3  26581  1wlkdlem3  26999  elunirn2  29451  fpwrelmap  29508  metidval  29933  pstmval  29938  brsiga  30246  measbase  30260  cvmsrcl  31246  snmlval  31313  fneuni  32342  uncf  33388  unccur  33392  caures  33556  ismtyval  33599  isismty  33600  heiborlem10  33619  eldiophb  37320  elmnc  37706  issdrg  37767  submgmrcl  41782  elbigofrcl  42344