Theorem ffvelrni 6266

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

Hypothesis

Ref	Expression
ffvrni.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

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

Proof of Theorem ffvelrni

Step	Hyp	Ref	Expression
1		ffvrni.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		ffvelrn 6265	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 702	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1977  ⟶wf 5800  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  f0cli  6278  cantnfval2  8449  cantnfle  8451  cantnflt  8452  cantnfres  8457  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  wemapwe  8477  cnfcomlem  8479  cnfcom  8480  cnfcom3lem  8483  cnfcom3  8484  ackbij1lem14  8938  ackbij1lem15  8939  ackbij1lem16  8940  ackbij1lem18  8942  fpwwe2lem8  9338  nqercl  9632  uzssz  11583  axdc4uzlem  12644  hashkf  12981  hashcl  13009  hashxrcl  13010  hashgadd  13027  cjcl  13693  limsupcl  14052  limsuplt  14058  limsupval2  14059  limsupgre  14060  limsupbnd2  14062  cn1lem  14176  climcn1lem  14181  caucvgrlem2  14253  fsumrelem  14380  ackbijnn  14399  efcl  14652  sincl  14695  coscl  14696  rpnnen2lem9  14790  rpnnen2lem12  14793  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadaddlem  15026  sadasslem  15030  sadeq  15032  algcvg  15127  algcvgb  15129  algcvga  15130  algfx  15131  eucalgcvga  15137  eucalg  15138  xpsaddlem  16058  xpsvsca  16062  xpsle  16064  efgtf  17958  efgtlen  17962  efginvrel2  17963  efginvrel1  17964  efgsp1  17973  efgredleme  17979  efgredlemc  17981  efgred  17984  efgred2  17989  efgcpbllemb  17991  frgpnabllem1  18099  xpsdsval  21996  xrhmeo  22553  ioorcl  23151  volsup2  23179  volivth  23181  itg2const2  23314  itg2gt0  23333  dvcjbr  23518  dvcj  23519  dvfre  23520  rolle  23557  deg1xrcl  23646  plypf1  23772  resinf1o  24086  efif1olem4  24095  eff1olem  24098  logrncl  24118  relogcl  24126  asincl  24400  acoscl  24402  atancl  24408  asinrebnd  24428  dvatan  24462  leibpilem2  24468  leibpi  24469  areacl  24489  areage0  24490  divsqrtsumo1  24510  emcllem6  24527  emcllem7  24528  gamcl  24570  chtcl  24635  chpcl  24650  ppicl  24657  mucl  24667  sqff1o  24708  bposlem7  24815  dchrisum0lem2a  25006  mulog2sumlem1  25023  pntrsumo1  25054  pntrsumbnd  25055  pntrsumbnd2  25056  selbergr  25057  selberg3r  25058  selberg34r  25060  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntlemn  25089  pntlemj  25092  pntlemf  25094  pntlemo  25096  pntleml  25100  vdegp1ai  26511  lnocoi  26996  nmlno0lem  27032  nmblolbii  27038  blocnilem  27043  blocni  27044  normcl  27366  occl  27547  hococli  28008  hosubcli  28012  hoaddcomi  28015  hodsi  28018  hoaddassi  28019  hocadddiri  28022  hocsubdiri  28023  ho2coi  28024  hoaddid1i  28029  ho0coi  28031  hoid1ri  28033  honegsubi  28039  ho01i  28071  ho02i  28072  dmadjrn  28138  nmopnegi  28208  lnopaddi  28214  lnopsubi  28217  hoddii  28232  nmlnop0iALT  28238  lnopmi  28243  lnophsi  28244  lnopcoi  28246  lnopeq0lem1  28248  lnopeqi  28251  lnopunilem1  28253  lnopunilem2  28254  lnophmlem2  28260  nmbdoplbi  28267  nmcopexi  28270  nmcoplbi  28271  nmophmi  28274  lnopconi  28277  lnfn0i  28285  lnfnaddi  28286  lnfnmuli  28287  lnfnsubi  28289  nmbdfnlbi  28292  nmcfnexi  28294  nmcfnlbi  28295  lnfnconi  28298  riesz3i  28305  riesz4i  28306  cnlnadjlem2  28311  cnlnadjlem4  28313  cnlnadjlem6  28315  cnlnadjlem7  28316  nmopadjlem  28332  nmoptrii  28337  nmopcoi  28338  adjcoi  28343  nmopcoadji  28344  bracnln  28352  opsqrlem5  28387  opsqrlem6  28388  hmopidmchi  28394  hmopidmpji  28395  pjsdii  28398  pjddii  28399  pjcohocli  28446  mhmhmeotmd  29301  xrge0pluscn  29314  voliune  29619  volfiniune  29620  ddemeas  29626  eulerpartlems  29749  eulerpartlemsv3  29750  eulerpartlemgc  29751  eulerpartlemgvv  29765  eulerpartlemgf  29768  eulerpartlemgs2  29769  eulerpartlemn  29770  derangen  30408  subfacf  30411  subfacp1lem6  30421  subfaclim  30424  subfacval3  30425  msrrcl  30694  msrid  30696  circum  30822  ismbl3  38879  ovolsplit  38881  stirlinglem13  38979  fourierdlem55  39054  fourierdlem77  39076  fourierdlem80  39079