Theorem elfvdm 6903

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

Syntax hints:   → wi 4   = wceq 1562   ∈ wcel 2144  ∅c0 4287  dom cdm 5649  ‘cfv 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-nul 5258  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-dm 5659  df-iota 6479  df-fv 6531

This theorem is referenced by:  elfvex  6904  elfvmptrab1w  7005  fveqdmss  7061  eldmrexrnb  7075  elmpocl  7639  elovmpt3rab1  7658  mpoxeldm  8193  mpoxopn0yelv  8195  mpoxopxnop0  8197  r1pwss  9744  rankwflemb  9753  r1elwf  9756  rankr1ai  9758  rankdmr1  9761  rankr1ag  9762  rankr1c  9781  r1pwcl  9807  cardne  9925  cardsdomelir  9933  r1wunlim  10697  eluzel2  12846  acsfiel  17688  homarcl2  18070  arwrcl  18079  pleval2i  18368  acsdrscl  18580  acsficl  18581  submgmrcl  18731  gsumws1  18874  cntzrcl  19369  smndlsmidm  19698  eldprd  20048  isunit  20424  isirred  20470  lbsss  21146  lbssp  21148  lbsind  21149  elocv  21722  cssi  21738  linds1  21864  linds2  21865  lindsind  21871  ply1frcl  22383  eltg4i  23022  eltg3  23024  tg1  23026  tg2  23027  cldrcl  23088  neiss2  23163  lmrcl  23293  iscnp2  23301  kqtop  23807  fbasne0  23892  0nelfb  23893  fbsspw  23894  fbasssin  23898  fbun  23902  trfbas2  23905  trfbas  23906  isfil  23909  filss  23915  fbasweak  23927  fgval  23932  elfg  23933  fgcl  23940  isufil  23965  ufilss  23967  trufil  23972  fmval  24005  elfm3  24012  fmfnfmlem4  24019  fmfnfm  24020  metflem  24390  xmetf  24391  xmeteq0  24400  xmettri2  24402  xmetres2  24423  blfvalps  24445  blvalps  24447  blval  24448  blfps  24468  blf  24469  isxms2  24510  tmslem  24544  lmmbr2  25323  lmmbrf  25326  fmcfil  25336  iscau2  25341  iscauf  25344  caucfil  25347  cmetcaulem  25352  iscmet3  25357  cfilresi  25359  caussi  25361  causs  25362  metcld2  25371  cmetss  25380  bcthlem1  25388  bcth3  25395  cpncn  26000  cpnres  26001  madebdayim  27983  oldbdayim  27984  newbdayim  27998  cutminmax  28031  tglngne  28721  wlkdlem3  29885  1wlkdlem3  30343  fpwrelmap  32937  brsiga  34482  measbase  34496  r1elcl  35398  cvmsrcl  35619  snmlval  35686  fneuni  36712  uncf  38103  unccur  38107  caures  38264  ismtyval  38304  isismty  38305  heiborlem10  38324  eldiophb  43343  elmnc  43718  elbigofrcl  49177  cicrcl2  49669  cic1st2nd  49673  eloppf  49759