Theorem ffvelcdmi 6988

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

Syntax hints:   → wi 4   ∈ wcel 2103  ⟶wf 6450  ‘cfv 6454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-12 2168  ax-ext 2706  ax-sep 5231  ax-nul 5238  ax-pr 5360

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3226  df-v 3438  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4844  df-br 5081  df-opab 5143  df-id 5496  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-fv 6462

This theorem is referenced by:  f0cli  7002  cantnfval2  9463  cantnfle  9465  cantnflt  9466  cantnfres  9471  cantnfp1lem3  9474  cantnflem1b  9480  cantnflem1d  9482  cantnflem1  9483  wemapwe  9491  cnfcomlem  9493  cnfcom  9494  cnfcom3lem  9497  cnfcom3  9498  ackbij1lem14  10025  ackbij1lem15  10026  ackbij1lem16  10027  ackbij1lem18  10029  fpwwe2lem7  10429  nqercl  10723  uzssz  12639  axdc4uzlem  13739  hashkf  14082  hashcl  14106  hashxrcl  14107  hashgadd  14127  cjcl  14851  limsupcl  15217  limsuplt  15223  limsupval2  15224  limsupgre  15225  limsupbnd2  15227  cn1lem  15342  climcn1lem  15347  caucvgrlem2  15421  fsumrelem  15554  ackbijnn  15575  efcl  15827  sincl  15870  coscl  15871  rpnnen2lem9  15966  rpnnen2lem12  15969  sadcaddlem  16199  sadadd2lem  16201  sadadd3  16203  sadaddlem  16208  sadasslem  16212  sadeq  16214  algcvg  16316  algcvgb  16318  algcvga  16319  algfx  16320  eucalgcvga  16326  eucalg  16327  xpsaddlem  17319  xpsvsca  17323  xpsle  17325  efgtf  19363  efgtlen  19367  efginvrel2  19368  efginvrel1  19369  efgsp1  19378  efgredleme  19384  efgredlemc  19386  efgred  19389  efgred2  19394  efgcpbllemb  19396  frgpnabllem1  19509  xpsdsval  23569  xrhmeo  24144  ioorcl  24776  volsup2  24804  volivth  24806  itg2const2  24941  itg2gt0  24960  dvcjbr  25148  dvcj  25149  dvfre  25150  rolle  25189  deg1xrcl  25282  plypf1  25408  resinf1o  25727  efif1olem4  25736  eff1olem  25739  logrncl  25758  relogcl  25766  asincl  26058  acoscl  26060  atancl  26066  asinrebnd  26086  dvatan  26120  leibpilem2  26126  leibpi  26127  areacl  26147  areage0  26148  divsqrtsumo1  26168  emcllem6  26185  emcllem7  26186  gamcl  26228  chtcl  26293  chpcl  26308  ppicl  26315  mucl  26325  sqff1o  26366  bposlem7  26473  dchrisum0lem2a  26700  mulog2sumlem1  26717  pntrsumo1  26748  pntrsumbnd  26749  pntrsumbnd2  26750  selbergr  26751  selberg3r  26752  selberg34r  26754  pntrlog2bndlem1  26760  pntrlog2bndlem2  26761  pntrlog2bndlem3  26762  pntrlog2bndlem4  26763  pntrlog2bndlem5  26764  pntrlog2bndlem6  26766  pntrlog2bnd  26767  pntpbnd1a  26768  pntpbnd1  26769  pntpbnd2  26770  pntibndlem2  26774  pntlemn  26783  pntlemj  26786  pntlemf  26788  pntlemo  26790  pntleml  26794  lnocoi  29154  nmlno0lem  29190  nmblolbii  29196  blocnilem  29201  blocni  29202  normcl  29522  occl  29701  hococli  30162  hosubcli  30166  hoaddcomi  30169  hodsi  30172  hoaddassi  30173  hocadddiri  30176  hocsubdiri  30177  ho2coi  30178  hoaddid1i  30183  ho0coi  30185  hoid1ri  30187  honegsubi  30193  ho01i  30225  ho02i  30226  dmadjrn  30292  nmopnegi  30362  lnopaddi  30368  lnopsubi  30371  hoddii  30386  nmlnop0iALT  30392  lnopmi  30397  lnophsi  30398  lnopcoi  30400  lnopeq0lem1  30402  lnopeqi  30405  lnopunilem1  30407  lnopunilem2  30408  lnophmlem2  30414  nmbdoplbi  30421  nmcopexi  30424  nmcoplbi  30425  nmophmi  30428  lnopconi  30431  lnfn0i  30439  lnfnaddi  30440  lnfnmuli  30441  lnfnsubi  30443  nmbdfnlbi  30446  nmcfnexi  30448  nmcfnlbi  30449  lnfnconi  30452  riesz3i  30459  riesz4i  30460  cnlnadjlem2  30465  cnlnadjlem4  30467  cnlnadjlem6  30469  cnlnadjlem7  30470  nmopadjlem  30486  nmoptrii  30491  nmopcoi  30492  adjcoi  30497  nmopcoadji  30498  bracnln  30506  opsqrlem5  30541  opsqrlem6  30542  hmopidmchi  30548  hmopidmpji  30549  pjsdii  30552  pjddii  30553  pjcohocli  30600  mhmhmeotmd  31912  xrge0pluscn  31925  voliune  32232  volfiniune  32233  ddemeas  32239  eulerpartlems  32362  eulerpartlemsv3  32363  eulerpartlemgc  32364  eulerpartlemgvv  32378  eulerpartlemgf  32381  eulerpartlemgs2  32382  eulerpartlemn  32383  derangen  33169  subfacf  33172  subfacp1lem6  33182  subfaclim  33185  subfacval3  33186  msrrcl  33540  msrid  33542  circum  33667  newf  34077  leftf  34084  rightf  34085  elmade  34086  ssltleft  34089  ssltright  34090  liminfval2  43351  ismbl3  43569  ovolsplit  43571  stirlinglem13  43669  fourierdlem55  43744  fourierdlem77  43766  fourierdlem80  43769