Theorem elfvdm 6866

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∅c0 4283  dom cdm 5622  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-dm 5632  df-iota 6446  df-fv 6498

This theorem is referenced by:  elfvex  6867  elfvmptrab1w  6966  fveqdmss  7021  eldmrexrnb  7035  elmpocl  7597  elovmpt3rab1  7616  mpoxeldm  8151  mpoxopn0yelv  8153  mpoxopxnop0  8155  r1pwss  9694  rankwflemb  9703  r1elwf  9706  rankr1ai  9708  rankdmr1  9711  rankr1ag  9712  rankr1c  9731  r1pwcl  9757  cardne  9875  cardsdomelir  9883  r1wunlim  10646  eluzel2  12754  acsfiel  17575  homarcl2  17957  arwrcl  17966  pleval2i  18255  acsdrscl  18467  acsficl  18468  submgmrcl  18618  gsumws1  18761  cntzrcl  19254  smndlsmidm  19583  eldprd  19933  isunit  20307  isirred  20353  lbsss  21027  lbssp  21029  lbsind  21030  elocv  21621  cssi  21637  linds1  21763  linds2  21764  lindsind  21770  ply1frcl  22260  eltg4i  22902  eltg3  22904  tg1  22906  tg2  22907  cldrcl  22968  neiss2  23043  lmrcl  23173  iscnp2  23181  kqtop  23687  fbasne0  23772  0nelfb  23773  fbsspw  23774  fbasssin  23778  fbun  23782  trfbas2  23785  trfbas  23786  isfil  23789  filss  23795  fbasweak  23807  fgval  23812  elfg  23813  fgcl  23820  isufil  23845  ufilss  23847  trufil  23852  fmval  23885  elfm3  23892  fmfnfmlem4  23899  fmfnfm  23900  metflem  24270  xmetf  24271  xmeteq0  24280  xmettri2  24282  xmetres2  24303  blfvalps  24325  blvalps  24327  blval  24328  blfps  24348  blf  24349  isxms2  24390  tmslem  24424  lmmbr2  25213  lmmbrf  25216  fmcfil  25226  iscau2  25231  iscauf  25234  caucfil  25237  cmetcaulem  25242  iscmet3  25247  cfilresi  25249  caussi  25251  causs  25252  metcld2  25261  cmetss  25270  bcthlem1  25278  bcth3  25285  cpncn  25892  cpnres  25893  madebdayim  27860  oldbdayim  27861  newbdayim  27875  tglngne  28571  wlkdlem3  29705  1wlkdlem3  30163  fpwrelmap  32761  brsiga  34289  measbase  34303  r1elcl  35203  cvmsrcl  35407  snmlval  35474  fneuni  36490  uncf  37739  unccur  37743  caures  37900  ismtyval  37940  isismty  37941  heiborlem10  37960  eldiophb  42941  elmnc  43320  elbigofrcl  48738  cicrcl2  49230  cic1st2nd  49234  eloppf  49320