Theorem elfvdm 6870

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4274  dom cdm 5626  ‘cfv 6494

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 5242  ax-pr 5372

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5636  df-iota 6450  df-fv 6502

This theorem is referenced by:  elfvex  6871  elfvmptrab1w  6971  fveqdmss  7026  eldmrexrnb  7040  elmpocl  7603  elovmpt3rab1  7622  mpoxeldm  8156  mpoxopn0yelv  8158  mpoxopxnop0  8160  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  21068  lbssp  21070  lbsind  21071  elocv  21662  cssi  21678  linds1  21804  linds2  21805  lindsind  21811  ply1frcl  22297  eltg4i  22939  eltg3  22941  tg1  22943  tg2  22944  cldrcl  23005  neiss2  23080  lmrcl  23210  iscnp2  23218  kqtop  23724  fbasne0  23809  0nelfb  23810  fbsspw  23811  fbasssin  23815  fbun  23819  trfbas2  23822  trfbas  23823  isfil  23826  filss  23832  fbasweak  23844  fgval  23849  elfg  23850  fgcl  23857  isufil  23882  ufilss  23884  trufil  23889  fmval  23922  elfm3  23929  fmfnfmlem4  23936  fmfnfm  23937  metflem  24307  xmetf  24308  xmeteq0  24317  xmettri2  24319  xmetres2  24340  blfvalps  24362  blvalps  24364  blval  24365  blfps  24385  blf  24386  isxms2  24427  tmslem  24461  lmmbr2  25240  lmmbrf  25243  fmcfil  25253  iscau2  25258  iscauf  25261  caucfil  25264  cmetcaulem  25269  iscmet3  25274  cfilresi  25276  caussi  25278  causs  25279  metcld2  25288  cmetss  25297  bcthlem1  25305  bcth3  25312  cpncn  25917  cpnres  25918  madebdayim  27898  oldbdayim  27899  newbdayim  27913  cutminmax  27946  tglngne  28636  wlkdlem3  29770  1wlkdlem3  30228  fpwrelmap  32825  brsiga  34347  measbase  34361  r1elcl  35261  cvmsrcl  35466  snmlval  35533  fneuni  36549  uncf  37938  unccur  37942  caures  38099  ismtyval  38139  isismty  38140  heiborlem10  38159  eldiophb  43207  elmnc  43586  elbigofrcl  49042  cicrcl2  49534  cic1st2nd  49538  eloppf  49624