Theorem elfvdm 6919

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 4285	. 2 ⊢ (𝐴 ∈ (𝐹‘𝐵) → ¬ (𝐹‘𝐵) = ∅)
2		ndmfv 6917	. 2 ⊢ (¬ 𝐵 ∈ dom 𝐹 → (𝐹‘𝐵) = ∅)
3	1, 2	nsyl2 142	1 ⊢ (𝐴 ∈ (𝐹‘𝐵) → 𝐵 ∈ dom 𝐹)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  ∅c0 4278  dom cdm 5650  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-dm 5660  df-iota 6494  df-fv 6546

This theorem is used by:  elfvex  6920  elfvmptrab1w  7021  fveqdmss  7078  eldmrexrnb  7092  elmpocl  7662  elovmpt3rab1  7681  mpoxeldm  8228  mpoxopn0yelv  8230  mpoxopxnop0  8232  uncf  8891  r1pwss  9791  rankwflemb  9800  rankwflembOLD  9801  r1elwf  9804  rankr1ai  9806  rankdmr1  9809  rankr1ag  9810  rankr1c  9830  r1pwcl  9861  cardne  10046  cardsdomelir  10054  r1wunlim  10822  eluzel2  12970  acsfiel  17828  homarcl2  18210  arwrcl  18219  pleval2i  18508  acsdrscl  18720  acsficl  18721  submgmrcl  18884  gsumws1  19034  cntzrcl  19541  smndlsmidm  19870  eldprd  20220  isunit  20603  isirred  20649  lbsss  21352  lbssp  21354  lbsind  21355  elocv  21974  cssi  21990  linds1  22116  linds2  22117  lindsind  22123  ply1frcl  22636  eltg4i  23278  eltg3  23280  tg1  23282  tg2  23283  cldrcl  23344  neiss2  23419  lmrcl  23549  iscnp2  23557  kqtop  24064  fbasne0  24149  0nelfb  24150  fbsspw  24151  fbasssin  24155  fbun  24159  trfbas2  24162  trfbas  24163  isfil  24166  filss  24172  fbasweak  24184  fgval  24189  elfg  24190  fgcl  24197  isufil  24222  ufilss  24224  trufil  24229  fmval  24262  elfm3  24269  fmfnfmlem4  24276  fmfnfm  24277  metflem  24647  xmetf  24648  xmeteq0  24657  xmettri2  24659  xmetres2  24680  blfvalps  24702  blvalps  24704  blval  24705  blfps  24725  blf  24726  isxms2  24767  tmslem  24801  lmmbr2  25580  lmmbrf  25583  fmcfil  25593  iscau2  25598  iscauf  25601  caucfil  25604  cmetcaulem  25609  iscmet3  25614  cfilresi  25616  caussi  25618  causs  25619  metcld2  25628  cmetss  25637  bcthlem1  25645  bcth3  25652  cpncn  26256  cpnres  26257  madebdayim  28274  oldbdayim  28275  newbdayim  28289  cutminmax  28322  tglngne  29013  wlkdlem3  30263  1wlkdlem3  30730  fpwrelmap  33325  brsiga  34816  measbase  34830  cvmsrcl  36029  snmlval  36096  fneuni  37135  unccur  38527  caures  38695  ismtyval  38735  isismty  38736  heiborlem10  38755  eldiophb  43768  elmnc  44138  elbigofrcl  49662  cicrcl2  50151  cic1st2nd  50155  eloppf  50241