Theorem elfvdm 6943

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∅c0 4333  dom cdm 5685  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-dm 5695  df-iota 6514  df-fv 6569

This theorem is referenced by:  elfvex  6944  elfvmptrab1w  7043  fveqdmss  7098  eldmrexrnb  7112  elunirn2OLD  7273  elmpocl  7674  elovmpt3rab1  7693  mpoxeldm  8236  mpoxopn0yelv  8238  mpoxopxnop0  8240  r1pwss  9824  rankwflemb  9833  r1elwf  9836  rankr1ai  9838  rankdmr1  9841  rankr1ag  9842  rankr1c  9861  r1pwcl  9887  cardne  10005  cardsdomelir  10013  r1wunlim  10777  eluzel2  12883  acsfiel  17697  homarcl2  18080  arwrcl  18089  pleval2i  18381  acsdrscl  18591  acsficl  18592  submgmrcl  18708  gsumws1  18851  cntzrcl  19345  smndlsmidm  19674  eldprd  20024  isunit  20373  isirred  20419  lbsss  21076  lbssp  21078  lbsind  21079  elocv  21686  cssi  21702  linds1  21830  linds2  21831  lindsind  21837  ply1frcl  22322  eltg4i  22967  eltg3  22969  tg1  22971  tg2  22972  cldrcl  23034  neiss2  23109  lmrcl  23239  iscnp2  23247  kqtop  23753  fbasne0  23838  0nelfb  23839  fbsspw  23840  fbasssin  23844  fbun  23848  trfbas2  23851  trfbas  23852  isfil  23855  filss  23861  fbasweak  23873  fgval  23878  elfg  23879  fgcl  23886  isufil  23911  ufilss  23913  trufil  23918  fmval  23951  elfm3  23958  fmfnfmlem4  23965  fmfnfm  23966  metflem  24338  xmetf  24339  xmeteq0  24348  xmettri2  24350  xmetres2  24371  blfvalps  24393  blvalps  24395  blval  24396  blfps  24416  blf  24417  isxms2  24458  tmslem  24494  tmslemOLD  24495  lmmbr2  25293  lmmbrf  25296  fmcfil  25306  iscau2  25311  iscauf  25314  caucfil  25317  cmetcaulem  25322  iscmet3  25327  cfilresi  25329  caussi  25331  causs  25332  metcld2  25341  cmetss  25350  bcthlem1  25358  bcth3  25365  cpncn  25972  cpnres  25973  madebdayim  27926  oldbdayim  27927  tglngne  28558  wlkdlem3  29702  1wlkdlem3  30158  fpwrelmap  32744  brsiga  34184  measbase  34198  cvmsrcl  35269  snmlval  35336  fneuni  36348  uncf  37606  unccur  37610  caures  37767  ismtyval  37807  isismty  37808  heiborlem10  37827  eldiophb  42768  elmnc  43148  elbigofrcl  48471