Theorem elfvdm 6869

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∅c0 4286  dom cdm 5625  ‘cfv 6493

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 5252  ax-pr 5378

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 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-dm 5635  df-iota 6449  df-fv 6501

This theorem is referenced by:  elfvex  6870  elfvmptrab1w  6970  fveqdmss  7025  eldmrexrnb  7039  elmpocl  7601  elovmpt3rab1  7620  mpoxeldm  8155  mpoxopn0yelv  8157  mpoxopxnop0  8159  r1pwss  9700  rankwflemb  9709  r1elwf  9712  rankr1ai  9714  rankdmr1  9717  rankr1ag  9718  rankr1c  9737  r1pwcl  9763  cardne  9881  cardsdomelir  9889  r1wunlim  10652  eluzel2  12760  acsfiel  17581  homarcl2  17963  arwrcl  17972  pleval2i  18261  acsdrscl  18473  acsficl  18474  submgmrcl  18624  gsumws1  18767  cntzrcl  19260  smndlsmidm  19589  eldprd  19939  isunit  20313  isirred  20359  lbsss  21033  lbssp  21035  lbsind  21036  elocv  21627  cssi  21643  linds1  21769  linds2  21770  lindsind  21776  ply1frcl  22266  eltg4i  22908  eltg3  22910  tg1  22912  tg2  22913  cldrcl  22974  neiss2  23049  lmrcl  23179  iscnp2  23187  kqtop  23693  fbasne0  23778  0nelfb  23779  fbsspw  23780  fbasssin  23784  fbun  23788  trfbas2  23791  trfbas  23792  isfil  23795  filss  23801  fbasweak  23813  fgval  23818  elfg  23819  fgcl  23826  isufil  23851  ufilss  23853  trufil  23858  fmval  23891  elfm3  23898  fmfnfmlem4  23905  fmfnfm  23906  metflem  24276  xmetf  24277  xmeteq0  24286  xmettri2  24288  xmetres2  24309  blfvalps  24331  blvalps  24333  blval  24334  blfps  24354  blf  24355  isxms2  24396  tmslem  24430  lmmbr2  25219  lmmbrf  25222  fmcfil  25232  iscau2  25237  iscauf  25240  caucfil  25243  cmetcaulem  25248  iscmet3  25253  cfilresi  25255  caussi  25257  causs  25258  metcld2  25267  cmetss  25276  bcthlem1  25284  bcth3  25291  cpncn  25898  cpnres  25899  madebdayim  27888  oldbdayim  27889  newbdayim  27903  cutminmax  27936  tglngne  28626  wlkdlem3  29760  1wlkdlem3  30218  fpwrelmap  32814  brsiga  34342  measbase  34356  r1elcl  35256  cvmsrcl  35460  snmlval  35527  fneuni  36543  uncf  37802  unccur  37806  caures  37963  ismtyval  38003  isismty  38004  heiborlem10  38023  eldiophb  43066  elmnc  43445  elbigofrcl  48863  cicrcl2  49355  cic1st2nd  49359  eloppf  49445