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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∅c0 4286  dom cdm 5663  ‘cfv 6541

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6497  df-fv 6549

This theorem is used by:  elfvex  6921  elfvmptrab1w  7022  fveqdmss  7078  eldmrexrnb  7092  elmpocl  7662  elovmpt3rab1  7681  mpoxeldm  8214  mpoxopn0yelv  8216  mpoxopxnop0  8218  r1pwss  9764  rankwflemb  9773  r1elwf  9776  rankr1ai  9778  rankdmr1  9781  rankr1ag  9782  rankr1c  9801  r1pwcl  9827  cardne  9968  cardsdomelir  9976  r1wunlim  10742  eluzel2  12888  acsfiel  17737  homarcl2  18119  arwrcl  18128  pleval2i  18417  acsdrscl  18629  acsficl  18630  submgmrcl  18790  gsumws1  18939  cntzrcl  19446  smndlsmidm  19775  eldprd  20125  isunit  20506  isirred  20552  lbsss  21253  lbssp  21255  lbsind  21256  elocv  21873  cssi  21889  linds1  22015  linds2  22016  lindsind  22022  ply1frcl  22533  eltg4i  23172  eltg3  23174  tg1  23176  tg2  23177  cldrcl  23238  neiss2  23313  lmrcl  23443  iscnp2  23451  kqtop  23958  fbasne0  24043  0nelfb  24044  fbsspw  24045  fbasssin  24049  fbun  24053  trfbas2  24056  trfbas  24057  isfil  24060  filss  24066  fbasweak  24078  fgval  24083  elfg  24084  fgcl  24091  isufil  24116  ufilss  24118  trufil  24123  fmval  24156  elfm3  24163  fmfnfmlem4  24170  fmfnfm  24171  metflem  24541  xmetf  24542  xmeteq0  24551  xmettri2  24553  xmetres2  24574  blfvalps  24596  blvalps  24598  blval  24599  blfps  24619  blf  24620  isxms2  24661  tmslem  24695  lmmbr2  25474  lmmbrf  25477  fmcfil  25487  iscau2  25492  iscauf  25495  caucfil  25498  cmetcaulem  25503  iscmet3  25508  cfilresi  25510  caussi  25512  causs  25513  metcld2  25522  cmetss  25531  bcthlem1  25539  bcth3  25546  cpncn  26151  cpnres  26152  madebdayim  28137  oldbdayim  28138  newbdayim  28152  cutminmax  28185  tglngne  28875  wlkdlem3  30095  1wlkdlem3  30562  fpwrelmap  33153  brsiga  34643  measbase  34657  r1elcl  35554  cvmsrcl  35798  snmlval  35865  fneuni  36920  uncf  38312  unccur  38316  caures  38474  ismtyval  38514  isismty  38515  heiborlem10  38534  eldiophb  43566  elmnc  43941  elbigofrcl  49407  cicrcl2  49898  cic1st2nd  49902  eloppf  49988