Theorem elfvdm 6874

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4273  dom cdm 5631  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-dm 5641  df-iota 6454  df-fv 6506

This theorem is referenced by:  elfvex  6875  elfvmptrab1w  6975  fveqdmss  7030  eldmrexrnb  7044  elmpocl  7608  elovmpt3rab1  7627  mpoxeldm  8161  mpoxopn0yelv  8163  mpoxopxnop0  8165  r1pwss  9708  rankwflemb  9717  r1elwf  9720  rankr1ai  9722  rankdmr1  9725  rankr1ag  9726  rankr1c  9745  r1pwcl  9771  cardne  9889  cardsdomelir  9897  r1wunlim  10660  eluzel2  12793  acsfiel  17620  homarcl2  18002  arwrcl  18011  pleval2i  18300  acsdrscl  18512  acsficl  18513  submgmrcl  18663  gsumws1  18806  cntzrcl  19302  smndlsmidm  19631  eldprd  19981  isunit  20353  isirred  20399  lbsss  21072  lbssp  21074  lbsind  21075  elocv  21648  cssi  21664  linds1  21790  linds2  21791  lindsind  21797  ply1frcl  22283  eltg4i  22925  eltg3  22927  tg1  22929  tg2  22930  cldrcl  22991  neiss2  23066  lmrcl  23196  iscnp2  23204  kqtop  23710  fbasne0  23795  0nelfb  23796  fbsspw  23797  fbasssin  23801  fbun  23805  trfbas2  23808  trfbas  23809  isfil  23812  filss  23818  fbasweak  23830  fgval  23835  elfg  23836  fgcl  23843  isufil  23868  ufilss  23870  trufil  23875  fmval  23908  elfm3  23915  fmfnfmlem4  23922  fmfnfm  23923  metflem  24293  xmetf  24294  xmeteq0  24303  xmettri2  24305  xmetres2  24326  blfvalps  24348  blvalps  24350  blval  24351  blfps  24371  blf  24372  isxms2  24413  tmslem  24447  lmmbr2  25226  lmmbrf  25229  fmcfil  25239  iscau2  25244  iscauf  25247  caucfil  25250  cmetcaulem  25255  iscmet3  25260  cfilresi  25262  caussi  25264  causs  25265  metcld2  25274  cmetss  25283  bcthlem1  25291  bcth3  25298  cpncn  25903  cpnres  25904  madebdayim  27880  oldbdayim  27881  newbdayim  27895  cutminmax  27928  tglngne  28618  wlkdlem3  29751  1wlkdlem3  30209  fpwrelmap  32806  brsiga  34327  measbase  34341  r1elcl  35241  cvmsrcl  35446  snmlval  35513  fneuni  36529  uncf  37920  unccur  37924  caures  38081  ismtyval  38121  isismty  38122  heiborlem10  38141  eldiophb  43189  elmnc  43564  elbigofrcl  49026  cicrcl2  49518  cic1st2nd  49522  eloppf  49608