Theorem ffvelcdmi 7089

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 7087	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 688	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2099  ⟶wf 6542  ‘cfv 6546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554

This theorem is referenced by:  f0cli  7104  cantnfval2  9705  cantnfle  9707  cantnflt  9708  cantnfres  9713  cantnfp1lem3  9716  cantnflem1b  9722  cantnflem1d  9724  cantnflem1  9725  wemapwe  9733  cnfcomlem  9735  cnfcom  9736  cnfcom3lem  9739  cnfcom3  9740  ackbij1lem14  10267  ackbij1lem15  10268  ackbij1lem16  10269  ackbij1lem18  10271  fpwwe2lem7  10671  nqercl  10965  uzssz  12889  axdc4uzlem  13997  hashkf  14344  hashcl  14368  hashxrcl  14369  hashgadd  14389  cjcl  15105  limsupcl  15470  limsuplt  15476  limsupval2  15477  limsupgre  15478  limsupbnd2  15480  cn1lem  15595  climcn1lem  15600  caucvgrlem2  15674  fsumrelem  15806  ackbijnn  15827  efcl  16079  sincl  16123  coscl  16124  rpnnen2lem9  16219  rpnnen2lem12  16222  sadcaddlem  16452  sadadd2lem  16454  sadadd3  16456  sadaddlem  16461  sadasslem  16465  sadeq  16467  algcvg  16572  algcvgb  16574  algcvga  16575  algfx  16576  eucalgcvga  16582  eucalg  16583  xpsaddlem  17583  xpsvsca  17587  xpsle  17589  efgtf  19716  efgtlen  19720  efginvrel2  19721  efginvrel1  19722  efgsp1  19731  efgredleme  19737  efgredlemc  19739  efgred  19742  efgred2  19747  efgcpbllemb  19749  frgpnabllem1  19867  xpsdsval  24375  xrhmeo  24959  ioorcl  25594  volsup2  25622  volivth  25624  itg2const2  25759  itg2gt0  25778  dvcjbr  25969  dvcj  25970  dvfre  25971  rolle  26010  deg1xrcl  26106  plypf1  26236  resinf1o  26560  efif1olem4  26569  eff1olem  26572  logrncl  26591  relogcl  26599  asincl  26898  acoscl  26900  atancl  26906  asinrebnd  26926  dvatan  26960  leibpilem2  26966  leibpi  26967  areacl  26987  areage0  26988  divsqrtsumo1  27009  emcllem6  27026  emcllem7  27027  gamcl  27069  chtcl  27134  chpcl  27149  ppicl  27156  mucl  27166  sqff1o  27207  bposlem7  27316  dchrisum0lem2a  27543  mulog2sumlem1  27560  pntrsumo1  27591  pntrsumbnd  27592  pntrsumbnd2  27593  selbergr  27594  selberg3r  27595  selberg34r  27597  pntrlog2bndlem1  27603  pntrlog2bndlem2  27604  pntrlog2bndlem3  27605  pntrlog2bndlem4  27606  pntrlog2bndlem5  27607  pntrlog2bndlem6  27609  pntrlog2bnd  27610  pntpbnd1a  27611  pntpbnd1  27612  pntpbnd2  27613  pntibndlem2  27617  pntlemn  27626  pntlemj  27629  pntlemf  27631  pntlemo  27633  pntleml  27637  newf  27879  leftf  27886  rightf  27887  elmade  27888  ssltleft  27891  ssltright  27892  lnocoi  30687  nmlno0lem  30723  nmblolbii  30729  blocnilem  30734  blocni  30735  normcl  31055  occl  31234  hococli  31695  hosubcli  31699  hoaddcomi  31702  hodsi  31705  hoaddassi  31706  hocadddiri  31709  hocsubdiri  31710  ho2coi  31711  hoaddridi  31716  ho0coi  31718  hoid1ri  31720  honegsubi  31726  ho01i  31758  ho02i  31759  dmadjrn  31825  nmopnegi  31895  lnopaddi  31901  lnopsubi  31904  hoddii  31919  nmlnop0iALT  31925  lnopmi  31930  lnophsi  31931  lnopcoi  31933  lnopeq0lem1  31935  lnopeqi  31938  lnopunilem1  31940  lnopunilem2  31941  lnophmlem2  31947  nmbdoplbi  31954  nmcopexi  31957  nmcoplbi  31958  nmophmi  31961  lnopconi  31964  lnfn0i  31972  lnfnaddi  31973  lnfnmuli  31974  lnfnsubi  31976  nmbdfnlbi  31979  nmcfnexi  31981  nmcfnlbi  31982  lnfnconi  31985  riesz3i  31992  riesz4i  31993  cnlnadjlem2  31998  cnlnadjlem4  32000  cnlnadjlem6  32002  cnlnadjlem7  32003  nmopadjlem  32019  nmoptrii  32024  nmopcoi  32025  adjcoi  32030  nmopcoadji  32031  bracnln  32039  opsqrlem5  32074  opsqrlem6  32075  hmopidmchi  32081  hmopidmpji  32082  pjsdii  32085  pjddii  32086  pjcohocli  32133  mhmhmeotmd  33755  xrge0pluscn  33768  voliune  34075  volfiniune  34076  ddemeas  34082  eulerpartlems  34207  eulerpartlemsv3  34208  eulerpartlemgc  34209  eulerpartlemgvv  34223  eulerpartlemgf  34226  eulerpartlemgs2  34227  eulerpartlemn  34228  derangen  35013  subfacf  35016  subfacp1lem6  35026  subfaclim  35029  subfacval3  35030  msrrcl  35384  msrid  35386  circum  35515  fpwfvss  43116  liminfval2  45425  ismbl3  45643  ovolsplit  45645  stirlinglem13  45743  fourierdlem55  45818  fourierdlem77  45840  fourierdlem80  45843