Theorem ffvelcdmi 7022

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

Syntax hints:   → wi 4   ∈ wcel 2113  ⟶wf 6482  ‘cfv 6486

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 5236  ax-nul 5246  ax-pr 5372

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 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494

This theorem is referenced by:  f0cli  7037  cantnfval2  9566  cantnfle  9568  cantnflt  9569  cantnfres  9574  cantnfp1lem3  9577  cantnflem1b  9583  cantnflem1d  9585  cantnflem1  9586  wemapwe  9594  cnfcomlem  9596  cnfcom  9597  cnfcom3lem  9600  cnfcom3  9601  ackbij1lem14  10130  ackbij1lem15  10131  ackbij1lem16  10132  ackbij1lem18  10134  fpwwe2lem7  10535  nqercl  10829  uzssz  12759  axdc4uzlem  13892  hashkf  14241  hashcl  14265  hashxrcl  14266  hashgadd  14286  cjcl  15014  limsupcl  15382  limsuplt  15388  limsupval2  15389  limsupgre  15390  limsupbnd2  15392  cn1lem  15507  climcn1lem  15512  caucvgrlem2  15584  fsumrelem  15716  ackbijnn  15737  efcl  15991  sincl  16037  coscl  16038  rpnnen2lem9  16133  rpnnen2lem12  16136  sadcaddlem  16370  sadadd2lem  16372  sadadd3  16374  sadaddlem  16379  sadasslem  16383  sadeq  16385  algcvg  16489  algcvgb  16491  algcvga  16492  algfx  16493  eucalgcvga  16499  eucalg  16500  xpsaddlem  17479  xpsvsca  17483  xpsle  17485  efgtf  19636  efgtlen  19640  efginvrel2  19641  efginvrel1  19642  efgsp1  19651  efgredleme  19657  efgredlemc  19659  efgred  19662  efgred2  19667  efgcpbllemb  19669  frgpnabllem1  19787  xpsdsval  24297  xrhmeo  24872  ioorcl  25506  volsup2  25534  volivth  25536  itg2const2  25670  itg2gt0  25689  dvcjbr  25881  dvcj  25882  dvfre  25883  rolle  25922  deg1xrcl  26015  plypf1  26145  resinf1o  26473  efif1olem4  26482  eff1olem  26485  logrncl  26504  relogcl  26512  asincl  26811  acoscl  26813  atancl  26819  asinrebnd  26839  dvatan  26873  leibpilem2  26879  leibpi  26880  areacl  26900  areage0  26901  divsqrtsumo1  26922  emcllem6  26939  emcllem7  26940  gamcl  26982  chtcl  27047  chpcl  27062  ppicl  27069  mucl  27079  sqff1o  27120  bposlem7  27229  dchrisum0lem2a  27456  mulog2sumlem1  27473  pntrsumo1  27504  pntrsumbnd  27505  pntrsumbnd2  27506  selbergr  27507  selberg3r  27508  selberg34r  27510  pntrlog2bndlem1  27516  pntrlog2bndlem2  27517  pntrlog2bndlem3  27518  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntrlog2bndlem6  27522  pntrlog2bnd  27523  pntpbnd1a  27524  pntpbnd1  27525  pntpbnd2  27526  pntibndlem2  27530  pntlemn  27539  pntlemj  27542  pntlemf  27544  pntlemo  27546  pntleml  27550  newf  27800  leftf  27811  rightf  27812  elmade  27813  ssltleft  27816  ssltright  27817  lnocoi  30739  nmlno0lem  30775  nmblolbii  30781  blocnilem  30786  blocni  30787  normcl  31107  occl  31286  hococli  31747  hosubcli  31751  hoaddcomi  31754  hodsi  31757  hoaddassi  31758  hocadddiri  31761  hocsubdiri  31762  ho2coi  31763  hoaddridi  31768  ho0coi  31770  hoid1ri  31772  honegsubi  31778  ho01i  31810  ho02i  31811  dmadjrn  31877  nmopnegi  31947  lnopaddi  31953  lnopsubi  31956  hoddii  31971  nmlnop0iALT  31977  lnopmi  31982  lnophsi  31983  lnopcoi  31985  lnopeq0lem1  31987  lnopeqi  31990  lnopunilem1  31992  lnopunilem2  31993  lnophmlem2  31999  nmbdoplbi  32006  nmcopexi  32009  nmcoplbi  32010  nmophmi  32013  lnopconi  32016  lnfn0i  32024  lnfnaddi  32025  lnfnmuli  32026  lnfnsubi  32028  nmbdfnlbi  32031  nmcfnexi  32033  nmcfnlbi  32034  lnfnconi  32037  riesz3i  32044  riesz4i  32045  cnlnadjlem2  32050  cnlnadjlem4  32052  cnlnadjlem6  32054  cnlnadjlem7  32055  nmopadjlem  32071  nmoptrii  32076  nmopcoi  32077  adjcoi  32082  nmopcoadji  32083  bracnln  32091  opsqrlem5  32126  opsqrlem6  32127  hmopidmchi  32133  hmopidmpji  32134  pjsdii  32137  pjddii  32138  pjcohocli  32185  mhmhmeotmd  33961  xrge0pluscn  33974  voliune  34263  volfiniune  34264  ddemeas  34270  eulerpartlems  34394  eulerpartlemsv3  34395  eulerpartlemgc  34396  eulerpartlemgvv  34410  eulerpartlemgf  34413  eulerpartlemgs2  34414  eulerpartlemn  34415  derangen  35237  subfacf  35240  subfacp1lem6  35250  subfaclim  35253  subfacval3  35254  msrrcl  35608  msrid  35610  circum  35739  fpwfvss  43529  liminfval2  45890  ismbl3  46108  ovolsplit  46110  stirlinglem13  46208  fourierdlem55  46283  fourierdlem77  46305  fourierdlem80  46308