Theorem elfvdm 6939

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∅c0 4281  dom cdm 5655  ‘cfv 6555

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-dm 5665  df-iota 6509  df-fv 6563

This theorem is used by:  elfvex  6940  elfvmptrab1w  7041  fveqdmss  7099  eldmrexrnb  7113  elmpocl  7683  elovmpt3rab1  7702  mpoxeldm  8253  mpoxopn0yelv  8255  mpoxopxnop0  8257  uncf  8916  r1pwss  9815  rankwflemb  9824  rankwflembOLD  9825  r1elwf  9828  rankr1ai  9830  rankdmr1  9833  rankr1ag  9834  rankr1c  9854  r1pwcl  9885  cardne  10070  cardsdomelir  10078  r1wunlim  10846  eluzel2  12994  acsfiel  17854  homarcl2  18236  arwrcl  18245  pleval2i  18534  acsdrscl  18746  acsficl  18747  submgmrcl  18910  gsumws1  19060  cntzrcl  19568  smndlsmidm  19897  eldprd  20247  isunit  20630  isirred  20676  lbsss  21379  lbssp  21381  lbsind  21382  elocv  22001  cssi  22017  linds1  22143  linds2  22144  lindsind  22150  ply1frcl  22663  eltg4i  23305  eltg3  23307  tg1  23309  tg2  23310  cldrcl  23371  neiss2  23446  lmrcl  23576  iscnp2  23584  kqtop  24091  fbasne0  24176  0nelfb  24177  fbsspw  24178  fbasssin  24182  fbun  24186  trfbas2  24189  trfbas  24190  isfil  24193  filss  24199  fbasweak  24211  fgval  24216  elfg  24217  fgcl  24224  isufil  24249  ufilss  24251  trufil  24256  fmval  24289  elfm3  24296  fmfnfmlem4  24303  fmfnfm  24304  metflem  24674  xmetf  24675  xmeteq0  24684  xmettri2  24686  xmetres2  24707  blfvalps  24729  blvalps  24731  blval  24732  blfps  24752  blf  24753  isxms2  24794  tmslem  24828  lmmbr2  25607  lmmbrf  25610  fmcfil  25620  iscau2  25625  iscauf  25628  caucfil  25631  cmetcaulem  25636  iscmet3  25641  cfilresi  25643  caussi  25645  causs  25646  metcld2  25655  cmetss  25664  bcthlem1  25672  bcth3  25679  cpncn  26283  cpnres  26284  madebdayim  28301  oldbdayim  28302  newbdayim  28316  cutminmax  28349  tglngne  29040  wlkdlem3  30290  1wlkdlem3  30757  fpwrelmap  33392  brsiga  34883  measbase  34897  cvmsrcl  36195  snmlval  36262  fneuni  37312  unccur  38717  caures  38885  ismtyval  38925  isismty  38926  heiborlem10  38945  eldiophb  43959  elmnc  44328  elbigofrcl  49865  cicrcl2  50360  cic1st2nd  50364  eloppf  50452