Theorem elfvdm 6915

Description: If a function value has a member, then the argument belongs to the domain. (An artifact of our function value definition.) (Contributed by NM, 12-Feb-2007.) (Proof shortened by BJ, 22-Oct-2022.)

Assertion

Ref	Expression
elfvdm	⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)

Proof of Theorem elfvdm

Step	Hyp	Ref	Expression
1		n0i 4293	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ¬ (𝐹‘𝐵) = ∅)
2		ndmfv 6913	. 2 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅)
3	1, 2	nsyl2 142	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2143  ∅c0 4286  dom cdm 5661  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-dm 5671  df-iota 6492  df-fv 6544

This theorem is used by:  elfvex  6916  elfvmptrab1w  7017  fveqdmss  7073  eldmrexrnb  7087  elmpocl  7651  elovmpt3rab1  7670  mpoxeldm  8203  mpoxopn0yelv  8205  mpoxopxnop0  8207  r1pwss  9752  rankwflemb  9761  r1elwf  9764  rankr1ai  9766  rankdmr1  9769  rankr1ag  9770  rankr1c  9789  r1pwcl  9815  cardne  9956  cardsdomelir  9964  r1wunlim  10726  eluzel2  12871  acsfiel  17714  homarcl2  18096  arwrcl  18105  pleval2i  18394  acsdrscl  18606  acsficl  18607  submgmrcl  18757  gsumws1  18901  cntzrcl  19401  smndlsmidm  19730  eldprd  20080  isunit  20460  isirred  20506  lbsss  21207  lbssp  21209  lbsind  21210  elocv  21827  cssi  21843  linds1  21969  linds2  21970  lindsind  21976  ply1frcl  22487  eltg4i  23126  eltg3  23128  tg1  23130  tg2  23131  cldrcl  23192  neiss2  23267  lmrcl  23397  iscnp2  23405  kqtop  23911  fbasne0  23996  0nelfb  23997  fbsspw  23998  fbasssin  24002  fbun  24006  trfbas2  24009  trfbas  24010  isfil  24013  filss  24019  fbasweak  24031  fgval  24036  elfg  24037  fgcl  24044  isufil  24069  ufilss  24071  trufil  24076  fmval  24109  elfm3  24116  fmfnfmlem4  24123  fmfnfm  24124  metflem  24494  xmetf  24495  xmeteq0  24504  xmettri2  24506  xmetres2  24527  blfvalps  24549  blvalps  24551  blval  24552  blfps  24572  blf  24573  isxms2  24614  tmslem  24648  lmmbr2  25427  lmmbrf  25430  fmcfil  25440  iscau2  25445  iscauf  25448  caucfil  25451  cmetcaulem  25456  iscmet3  25461  cfilresi  25463  caussi  25465  causs  25466  metcld2  25475  cmetss  25484  bcthlem1  25492  bcth3  25499  cpncn  26104  cpnres  26105  madebdayim  28090  oldbdayim  28091  newbdayim  28105  cutminmax  28138  tglngne  28828  wlkdlem3  30041  1wlkdlem3  30499  fpwrelmap  33087  brsiga  34582  measbase  34596  r1elcl  35500  cvmsrcl  35764  snmlval  35831  fneuni  36886  uncf  38278  unccur  38282  caures  38439  ismtyval  38479  isismty  38480  heiborlem10  38499  eldiophb  43516  elmnc  43891  elbigofrcl  49358  cicrcl2  49849  cic1st2nd  49853  eloppf  49939