Theorem ffvelcdmi 7016

Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)

Hypothesis

Ref	Expression
ffvelcdmi.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

Ref	Expression
ffvelcdmi	⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdmi

Step	Hyp	Ref	Expression
1		ffvelcdmi.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		ffvelcdm 7014	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 690	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2111  ⟶wf 6477  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489

This theorem is referenced by:  f0cli  7031  cantnfval2  9559  cantnfle  9561  cantnflt  9562  cantnfres  9567  cantnfp1lem3  9570  cantnflem1b  9576  cantnflem1d  9578  cantnflem1  9579  wemapwe  9587  cnfcomlem  9589  cnfcom  9590  cnfcom3lem  9593  cnfcom3  9594  ackbij1lem14  10120  ackbij1lem15  10121  ackbij1lem16  10122  ackbij1lem18  10124  fpwwe2lem7  10525  nqercl  10819  uzssz  12750  axdc4uzlem  13887  hashkf  14236  hashcl  14260  hashxrcl  14261  hashgadd  14281  cjcl  15009  limsupcl  15377  limsuplt  15383  limsupval2  15384  limsupgre  15385  limsupbnd2  15387  cn1lem  15502  climcn1lem  15507  caucvgrlem2  15579  fsumrelem  15711  ackbijnn  15732  efcl  15986  sincl  16032  coscl  16033  rpnnen2lem9  16128  rpnnen2lem12  16131  sadcaddlem  16365  sadadd2lem  16367  sadadd3  16369  sadaddlem  16374  sadasslem  16378  sadeq  16380  algcvg  16484  algcvgb  16486  algcvga  16487  algfx  16488  eucalgcvga  16494  eucalg  16495  xpsaddlem  17474  xpsvsca  17478  xpsle  17480  efgtf  19632  efgtlen  19636  efginvrel2  19637  efginvrel1  19638  efgsp1  19647  efgredleme  19653  efgredlemc  19655  efgred  19658  efgred2  19663  efgcpbllemb  19665  frgpnabllem1  19783  xpsdsval  24294  xrhmeo  24869  ioorcl  25503  volsup2  25531  volivth  25533  itg2const2  25667  itg2gt0  25686  dvcjbr  25878  dvcj  25879  dvfre  25880  rolle  25919  deg1xrcl  26012  plypf1  26142  resinf1o  26470  efif1olem4  26479  eff1olem  26482  logrncl  26501  relogcl  26509  asincl  26808  acoscl  26810  atancl  26816  asinrebnd  26836  dvatan  26870  leibpilem2  26876  leibpi  26877  areacl  26897  areage0  26898  divsqrtsumo1  26919  emcllem6  26936  emcllem7  26937  gamcl  26979  chtcl  27044  chpcl  27059  ppicl  27066  mucl  27076  sqff1o  27117  bposlem7  27226  dchrisum0lem2a  27453  mulog2sumlem1  27470  pntrsumo1  27501  pntrsumbnd  27502  pntrsumbnd2  27503  selbergr  27504  selberg3r  27505  selberg34r  27507  pntrlog2bndlem1  27513  pntrlog2bndlem2  27514  pntrlog2bndlem3  27515  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  pntrlog2bndlem6  27519  pntrlog2bnd  27520  pntpbnd1a  27521  pntpbnd1  27522  pntpbnd2  27523  pntibndlem2  27527  pntlemn  27536  pntlemj  27539  pntlemf  27541  pntlemo  27543  pntleml  27547  newf  27797  leftf  27808  rightf  27809  elmade  27810  ssltleft  27813  ssltright  27814  lnocoi  30732  nmlno0lem  30768  nmblolbii  30774  blocnilem  30779  blocni  30780  normcl  31100  occl  31279  hococli  31740  hosubcli  31744  hoaddcomi  31747  hodsi  31750  hoaddassi  31751  hocadddiri  31754  hocsubdiri  31755  ho2coi  31756  hoaddridi  31761  ho0coi  31763  hoid1ri  31765  honegsubi  31771  ho01i  31803  ho02i  31804  dmadjrn  31870  nmopnegi  31940  lnopaddi  31946  lnopsubi  31949  hoddii  31964  nmlnop0iALT  31970  lnopmi  31975  lnophsi  31976  lnopcoi  31978  lnopeq0lem1  31980  lnopeqi  31983  lnopunilem1  31985  lnopunilem2  31986  lnophmlem2  31992  nmbdoplbi  31999  nmcopexi  32002  nmcoplbi  32003  nmophmi  32006  lnopconi  32009  lnfn0i  32017  lnfnaddi  32018  lnfnmuli  32019  lnfnsubi  32021  nmbdfnlbi  32024  nmcfnexi  32026  nmcfnlbi  32027  lnfnconi  32030  riesz3i  32037  riesz4i  32038  cnlnadjlem2  32043  cnlnadjlem4  32045  cnlnadjlem6  32047  cnlnadjlem7  32048  nmopadjlem  32064  nmoptrii  32069  nmopcoi  32070  adjcoi  32075  nmopcoadji  32076  bracnln  32084  opsqrlem5  32119  opsqrlem6  32120  hmopidmchi  32126  hmopidmpji  32127  pjsdii  32130  pjddii  32131  pjcohocli  32178  mhmhmeotmd  33935  xrge0pluscn  33948  voliune  34237  volfiniune  34238  ddemeas  34244  eulerpartlems  34368  eulerpartlemsv3  34369  eulerpartlemgc  34370  eulerpartlemgvv  34384  eulerpartlemgf  34387  eulerpartlemgs2  34388  eulerpartlemn  34389  derangen  35204  subfacf  35207  subfacp1lem6  35217  subfaclim  35220  subfacval3  35221  msrrcl  35575  msrid  35577  circum  35706  fpwfvss  43444  liminfval2  45805  ismbl3  46023  ovolsplit  46025  stirlinglem13  46123  fourierdlem55  46198  fourierdlem77  46220  fourierdlem80  46223