Theorem ffvelcdmi 7025

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

Syntax hints:   → wi 4   ∈ wcel 2113  ⟶wf 6485  ‘cfv 6489

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 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497

This theorem is referenced by:  f0cli  7040  cantnfval2  9569  cantnfle  9571  cantnflt  9572  cantnfres  9577  cantnfp1lem3  9580  cantnflem1b  9586  cantnflem1d  9588  cantnflem1  9589  wemapwe  9597  cnfcomlem  9599  cnfcom  9600  cnfcom3lem  9603  cnfcom3  9604  ackbij1lem14  10133  ackbij1lem15  10134  ackbij1lem16  10135  ackbij1lem18  10137  fpwwe2lem7  10538  nqercl  10832  uzssz  12763  axdc4uzlem  13900  hashkf  14249  hashcl  14273  hashxrcl  14274  hashgadd  14294  cjcl  15022  limsupcl  15390  limsuplt  15396  limsupval2  15397  limsupgre  15398  limsupbnd2  15400  cn1lem  15515  climcn1lem  15520  caucvgrlem2  15592  fsumrelem  15724  ackbijnn  15745  efcl  15999  sincl  16045  coscl  16046  rpnnen2lem9  16141  rpnnen2lem12  16144  sadcaddlem  16378  sadadd2lem  16380  sadadd3  16382  sadaddlem  16387  sadasslem  16391  sadeq  16393  algcvg  16497  algcvgb  16499  algcvga  16500  algfx  16501  eucalgcvga  16507  eucalg  16508  xpsaddlem  17487  xpsvsca  17491  xpsle  17493  efgtf  19644  efgtlen  19648  efginvrel2  19649  efginvrel1  19650  efgsp1  19659  efgredleme  19665  efgredlemc  19667  efgred  19670  efgred2  19675  efgcpbllemb  19677  frgpnabllem1  19795  xpsdsval  24306  xrhmeo  24881  ioorcl  25515  volsup2  25543  volivth  25545  itg2const2  25679  itg2gt0  25698  dvcjbr  25890  dvcj  25891  dvfre  25892  rolle  25931  deg1xrcl  26024  plypf1  26154  resinf1o  26482  efif1olem4  26491  eff1olem  26494  logrncl  26513  relogcl  26521  asincl  26820  acoscl  26822  atancl  26828  asinrebnd  26848  dvatan  26882  leibpilem2  26888  leibpi  26889  areacl  26909  areage0  26910  divsqrtsumo1  26931  emcllem6  26948  emcllem7  26949  gamcl  26991  chtcl  27056  chpcl  27071  ppicl  27078  mucl  27088  sqff1o  27129  bposlem7  27238  dchrisum0lem2a  27465  mulog2sumlem1  27482  pntrsumo1  27513  pntrsumbnd  27514  pntrsumbnd2  27515  selbergr  27516  selberg3r  27517  selberg34r  27519  pntrlog2bndlem1  27525  pntrlog2bndlem2  27526  pntrlog2bndlem3  27527  pntrlog2bndlem4  27528  pntrlog2bndlem5  27529  pntrlog2bndlem6  27531  pntrlog2bnd  27532  pntpbnd1a  27533  pntpbnd1  27534  pntpbnd2  27535  pntibndlem2  27539  pntlemn  27548  pntlemj  27551  pntlemf  27553  pntlemo  27555  pntleml  27559  newf  27809  leftf  27820  rightf  27821  elmade  27822  ssltleft  27825  ssltright  27826  lnocoi  30748  nmlno0lem  30784  nmblolbii  30790  blocnilem  30795  blocni  30796  normcl  31116  occl  31295  hococli  31756  hosubcli  31760  hoaddcomi  31763  hodsi  31766  hoaddassi  31767  hocadddiri  31770  hocsubdiri  31771  ho2coi  31772  hoaddridi  31777  ho0coi  31779  hoid1ri  31781  honegsubi  31787  ho01i  31819  ho02i  31820  dmadjrn  31886  nmopnegi  31956  lnopaddi  31962  lnopsubi  31965  hoddii  31980  nmlnop0iALT  31986  lnopmi  31991  lnophsi  31992  lnopcoi  31994  lnopeq0lem1  31996  lnopeqi  31999  lnopunilem1  32001  lnopunilem2  32002  lnophmlem2  32008  nmbdoplbi  32015  nmcopexi  32018  nmcoplbi  32019  nmophmi  32022  lnopconi  32025  lnfn0i  32033  lnfnaddi  32034  lnfnmuli  32035  lnfnsubi  32037  nmbdfnlbi  32040  nmcfnexi  32042  nmcfnlbi  32043  lnfnconi  32046  riesz3i  32053  riesz4i  32054  cnlnadjlem2  32059  cnlnadjlem4  32061  cnlnadjlem6  32063  cnlnadjlem7  32064  nmopadjlem  32080  nmoptrii  32085  nmopcoi  32086  adjcoi  32091  nmopcoadji  32092  bracnln  32100  opsqrlem5  32135  opsqrlem6  32136  hmopidmchi  32142  hmopidmpji  32143  pjsdii  32146  pjddii  32147  pjcohocli  32194  mhmhmeotmd  33951  xrge0pluscn  33964  voliune  34253  volfiniune  34254  ddemeas  34260  eulerpartlems  34384  eulerpartlemsv3  34385  eulerpartlemgc  34386  eulerpartlemgvv  34400  eulerpartlemgf  34403  eulerpartlemgs2  34404  eulerpartlemn  34405  derangen  35227  subfacf  35230  subfacp1lem6  35240  subfaclim  35243  subfacval3  35244  msrrcl  35598  msrid  35600  circum  35729  fpwfvss  43519  liminfval2  45880  ismbl3  46098  ovolsplit  46100  stirlinglem13  46198  fourierdlem55  46273  fourierdlem77  46295  fourierdlem80  46298