Theorem elfvdm 6878

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4287  dom cdm 5634  ‘cfv 6502

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 2709  ax-nul 5255  ax-pr 5381

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-dm 5644  df-iota 6458  df-fv 6510

This theorem is referenced by:  elfvex  6879  elfvmptrab1w  6979  fveqdmss  7034  eldmrexrnb  7048  elmpocl  7611  elovmpt3rab1  7630  mpoxeldm  8165  mpoxopn0yelv  8167  mpoxopxnop0  8169  r1pwss  9710  rankwflemb  9719  r1elwf  9722  rankr1ai  9724  rankdmr1  9727  rankr1ag  9728  rankr1c  9747  r1pwcl  9773  cardne  9891  cardsdomelir  9899  r1wunlim  10662  eluzel2  12770  acsfiel  17591  homarcl2  17973  arwrcl  17982  pleval2i  18271  acsdrscl  18483  acsficl  18484  submgmrcl  18634  gsumws1  18777  cntzrcl  19273  smndlsmidm  19602  eldprd  19952  isunit  20326  isirred  20372  lbsss  21046  lbssp  21048  lbsind  21049  elocv  21640  cssi  21656  linds1  21782  linds2  21783  lindsind  21789  ply1frcl  22279  eltg4i  22921  eltg3  22923  tg1  22925  tg2  22926  cldrcl  22987  neiss2  23062  lmrcl  23192  iscnp2  23200  kqtop  23706  fbasne0  23791  0nelfb  23792  fbsspw  23793  fbasssin  23797  fbun  23801  trfbas2  23804  trfbas  23805  isfil  23808  filss  23814  fbasweak  23826  fgval  23831  elfg  23832  fgcl  23839  isufil  23864  ufilss  23866  trufil  23871  fmval  23904  elfm3  23911  fmfnfmlem4  23918  fmfnfm  23919  metflem  24289  xmetf  24290  xmeteq0  24299  xmettri2  24301  xmetres2  24322  blfvalps  24344  blvalps  24346  blval  24347  blfps  24367  blf  24368  isxms2  24409  tmslem  24443  lmmbr2  25232  lmmbrf  25235  fmcfil  25245  iscau2  25250  iscauf  25253  caucfil  25256  cmetcaulem  25261  iscmet3  25266  cfilresi  25268  caussi  25270  causs  25271  metcld2  25280  cmetss  25289  bcthlem1  25297  bcth3  25304  cpncn  25911  cpnres  25912  madebdayim  27901  oldbdayim  27902  newbdayim  27916  cutminmax  27949  tglngne  28640  wlkdlem3  29774  1wlkdlem3  30232  fpwrelmap  32829  brsiga  34367  measbase  34381  r1elcl  35281  cvmsrcl  35486  snmlval  35553  fneuni  36569  uncf  37879  unccur  37883  caures  38040  ismtyval  38080  isismty  38081  heiborlem10  38100  eldiophb  43143  elmnc  43522  elbigofrcl  48939  cicrcl2  49431  cic1st2nd  49435  eloppf  49521