Theorem elfvdm 6920

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∅c0 4279  dom cdm 5651  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-rab 3414  df-v 3453  df-dif 3900  df-un 3902  df-ss 3915  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-dm 5661  df-iota 6495  df-fv 6547

This theorem is used by:  elfvex  6921  elfvmptrab1w  7022  fveqdmss  7079  eldmrexrnb  7093  elmpocl  7663  elovmpt3rab1  7682  mpoxeldm  8229  mpoxopn0yelv  8231  mpoxopxnop0  8233  uncf  8892  r1pwss  9792  rankwflemb  9801  rankwflembOLD  9802  r1elwf  9805  rankr1ai  9807  rankdmr1  9810  rankr1ag  9811  rankr1c  9831  r1pwcl  9862  cardne  10047  cardsdomelir  10055  r1wunlim  10823  eluzel2  12971  acsfiel  17829  homarcl2  18211  arwrcl  18220  pleval2i  18509  acsdrscl  18721  acsficl  18722  submgmrcl  18885  gsumws1  19035  cntzrcl  19542  smndlsmidm  19871  eldprd  20221  isunit  20604  isirred  20650  lbsss  21353  lbssp  21355  lbsind  21356  elocv  21975  cssi  21991  linds1  22117  linds2  22118  lindsind  22124  ply1frcl  22637  eltg4i  23279  eltg3  23281  tg1  23283  tg2  23284  cldrcl  23345  neiss2  23420  lmrcl  23550  iscnp2  23558  kqtop  24065  fbasne0  24150  0nelfb  24151  fbsspw  24152  fbasssin  24156  fbun  24160  trfbas2  24163  trfbas  24164  isfil  24167  filss  24173  fbasweak  24185  fgval  24190  elfg  24191  fgcl  24198  isufil  24223  ufilss  24225  trufil  24230  fmval  24263  elfm3  24270  fmfnfmlem4  24277  fmfnfm  24278  metflem  24648  xmetf  24649  xmeteq0  24658  xmettri2  24660  xmetres2  24681  blfvalps  24703  blvalps  24705  blval  24706  blfps  24726  blf  24727  isxms2  24768  tmslem  24802  lmmbr2  25581  lmmbrf  25584  fmcfil  25594  iscau2  25599  iscauf  25602  caucfil  25605  cmetcaulem  25610  iscmet3  25615  cfilresi  25617  caussi  25619  causs  25620  metcld2  25629  cmetss  25638  bcthlem1  25646  bcth3  25653  cpncn  26257  cpnres  26258  madebdayim  28275  oldbdayim  28276  newbdayim  28290  cutminmax  28323  tglngne  29014  wlkdlem3  30264  1wlkdlem3  30731  fpwrelmap  33326  brsiga  34817  measbase  34831  cvmsrcl  36030  snmlval  36097  fneuni  37136  unccur  38528  caures  38696  ismtyval  38736  isismty  38737  heiborlem10  38756  eldiophb  43769  elmnc  44139  elbigofrcl  49663  cicrcl2  50152  cic1st2nd  50156  eloppf  50242