Theorem elfvdm 6895

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∅c0 4296  dom cdm 5638  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-dm 5648  df-iota 6464  df-fv 6519

This theorem is referenced by:  elfvex  6896  elfvmptrab1w  6995  fveqdmss  7050  eldmrexrnb  7064  elunirn2OLD  7227  elmpocl  7630  elovmpt3rab1  7649  mpoxeldm  8190  mpoxopn0yelv  8192  mpoxopxnop0  8194  r1pwss  9737  rankwflemb  9746  r1elwf  9749  rankr1ai  9751  rankdmr1  9754  rankr1ag  9755  rankr1c  9774  r1pwcl  9800  cardne  9918  cardsdomelir  9926  r1wunlim  10690  eluzel2  12798  acsfiel  17615  homarcl2  17997  arwrcl  18006  pleval2i  18295  acsdrscl  18505  acsficl  18506  submgmrcl  18622  gsumws1  18765  cntzrcl  19259  smndlsmidm  19586  eldprd  19936  isunit  20282  isirred  20328  lbsss  20984  lbssp  20986  lbsind  20987  elocv  21577  cssi  21593  linds1  21719  linds2  21720  lindsind  21726  ply1frcl  22205  eltg4i  22847  eltg3  22849  tg1  22851  tg2  22852  cldrcl  22913  neiss2  22988  lmrcl  23118  iscnp2  23126  kqtop  23632  fbasne0  23717  0nelfb  23718  fbsspw  23719  fbasssin  23723  fbun  23727  trfbas2  23730  trfbas  23731  isfil  23734  filss  23740  fbasweak  23752  fgval  23757  elfg  23758  fgcl  23765  isufil  23790  ufilss  23792  trufil  23797  fmval  23830  elfm3  23837  fmfnfmlem4  23844  fmfnfm  23845  metflem  24216  xmetf  24217  xmeteq0  24226  xmettri2  24228  xmetres2  24249  blfvalps  24271  blvalps  24273  blval  24274  blfps  24294  blf  24295  isxms2  24336  tmslem  24370  lmmbr2  25159  lmmbrf  25162  fmcfil  25172  iscau2  25177  iscauf  25180  caucfil  25183  cmetcaulem  25188  iscmet3  25193  cfilresi  25195  caussi  25197  causs  25198  metcld2  25207  cmetss  25216  bcthlem1  25224  bcth3  25231  cpncn  25838  cpnres  25839  madebdayim  27799  oldbdayim  27800  newbdayim  27814  tglngne  28477  wlkdlem3  29612  1wlkdlem3  30068  fpwrelmap  32656  brsiga  34173  measbase  34187  cvmsrcl  35251  snmlval  35318  fneuni  36335  uncf  37593  unccur  37597  caures  37754  ismtyval  37794  isismty  37795  heiborlem10  37814  eldiophb  42745  elmnc  43125  elbigofrcl  48539  cicrcl2  49032  cic1st2nd  49036  eloppf  49122