Theorem elfvdm 6865

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

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121  ∅c0 4264  dom cdm 5621  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5231  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-dm 5631  df-iota 6445  df-fv 6497

This theorem is referenced by:  elfvex  6866  elfvmptrab1w  6967  fveqdmss  7023  eldmrexrnb  7037  elmpocl  7601  elovmpt3rab1  7620  mpoxeldm  8155  mpoxopn0yelv  8157  mpoxopxnop0  8159  r1pwss  9703  rankwflemb  9712  r1elwf  9715  rankr1ai  9717  rankdmr1  9720  rankr1ag  9721  rankr1c  9740  r1pwcl  9766  cardne  9884  cardsdomelir  9892  r1wunlim  10655  eluzel2  12788  acsfiel  17615  homarcl2  17997  arwrcl  18006  pleval2i  18295  acsdrscl  18507  acsficl  18508  submgmrcl  18658  gsumws1  18801  cntzrcl  19297  smndlsmidm  19626  eldprd  19976  isunit  20348  isirred  20394  lbsss  21071  lbssp  21073  lbsind  21074  elocv  21647  cssi  21663  linds1  21789  linds2  21790  lindsind  21796  ply1frcl  22308  eltg4i  22947  eltg3  22949  tg1  22951  tg2  22952  cldrcl  23013  neiss2  23088  lmrcl  23218  iscnp2  23226  kqtop  23732  fbasne0  23817  0nelfb  23818  fbsspw  23819  fbasssin  23823  fbun  23827  trfbas2  23830  trfbas  23831  isfil  23834  filss  23840  fbasweak  23852  fgval  23857  elfg  23858  fgcl  23865  isufil  23890  ufilss  23892  trufil  23897  fmval  23930  elfm3  23937  fmfnfmlem4  23944  fmfnfm  23945  metflem  24315  xmetf  24316  xmeteq0  24325  xmettri2  24327  xmetres2  24348  blfvalps  24370  blvalps  24372  blval  24373  blfps  24393  blf  24394  isxms2  24435  tmslem  24469  lmmbr2  25248  lmmbrf  25251  fmcfil  25261  iscau2  25266  iscauf  25269  caucfil  25272  cmetcaulem  25277  iscmet3  25282  cfilresi  25284  caussi  25286  causs  25287  metcld2  25296  cmetss  25305  bcthlem1  25313  bcth3  25320  cpncn  25925  cpnres  25926  madebdayim  27902  oldbdayim  27903  newbdayim  27917  cutminmax  27950  tglngne  28640  wlkdlem3  29773  1wlkdlem3  30231  fpwrelmap  32829  brsiga  34379  measbase  34393  r1elcl  35294  cvmsrcl  35507  snmlval  35574  fneuni  36590  uncf  37981  unccur  37985  caures  38142  ismtyval  38182  isismty  38183  heiborlem10  38202  eldiophb  43221  elmnc  43596  elbigofrcl  49055  cicrcl2  49547  cic1st2nd  49551  eloppf  49637