Theorem ffvelrni 6720

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

Syntax hints:   → wi 4   ∈ wcel 2081  ⟶wf 6226  ‘cfv 6230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pr 5226

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-id 5353  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-fv 6238

This theorem is referenced by:  f0cli  6732  cantnfval2  8983  cantnfle  8985  cantnflt  8986  cantnfres  8991  cantnfp1lem3  8994  cantnflem1b  9000  cantnflem1d  9002  cantnflem1  9003  wemapwe  9011  cnfcomlem  9013  cnfcom  9014  cnfcom3lem  9017  cnfcom3  9018  ackbij1lem14  9506  ackbij1lem15  9507  ackbij1lem16  9508  ackbij1lem18  9510  fpwwe2lem8  9910  nqercl  10204  uzssz  12118  axdc4uzlem  13206  hashkf  13547  hashcl  13572  hashxrcl  13573  hashgadd  13591  cjcl  14303  limsupcl  14669  limsuplt  14675  limsupval2  14676  limsupgre  14677  limsupbnd2  14679  cn1lem  14793  climcn1lem  14798  caucvgrlem2  14870  fsumrelem  15000  ackbijnn  15021  efcl  15274  sincl  15317  coscl  15318  rpnnen2lem9  15413  rpnnen2lem12  15416  sadcaddlem  15644  sadadd2lem  15646  sadadd3  15648  sadaddlem  15653  sadasslem  15657  sadeq  15659  algcvg  15754  algcvgb  15756  algcvga  15757  algfx  15758  eucalgcvga  15764  eucalg  15765  xpsaddlem  16680  xpsvsca  16684  xpsle  16686  efgtf  18580  efgtlen  18584  efginvrel2  18585  efginvrel1  18586  efgsp1  18595  efgredleme  18601  efgredlemc  18603  efgred  18606  efgred2  18611  efgcpbllemb  18613  frgpnabllem1  18721  xpsdsval  22679  xrhmeo  23238  ioorcl  23866  volsup2  23894  volivth  23896  itg2const2  24030  itg2gt0  24049  dvcjbr  24234  dvcj  24235  dvfre  24236  rolle  24275  deg1xrcl  24364  plypf1  24490  resinf1o  24806  efif1olem4  24815  eff1olem  24818  logrncl  24837  relogcl  24845  asincl  25137  acoscl  25139  atancl  25145  asinrebnd  25165  dvatan  25199  leibpilem2  25206  leibpi  25207  areacl  25227  areage0  25228  divsqrtsumo1  25248  emcllem6  25265  emcllem7  25266  gamcl  25308  chtcl  25373  chpcl  25388  ppicl  25395  mucl  25405  sqff1o  25446  bposlem7  25553  dchrisum0lem2a  25780  mulog2sumlem1  25797  pntrsumo1  25828  pntrsumbnd  25829  pntrsumbnd2  25830  selbergr  25831  selberg3r  25832  selberg34r  25834  pntrlog2bndlem1  25840  pntrlog2bndlem2  25841  pntrlog2bndlem3  25842  pntrlog2bndlem4  25843  pntrlog2bndlem5  25844  pntrlog2bndlem6  25846  pntrlog2bnd  25847  pntpbnd1a  25848  pntpbnd1  25849  pntpbnd2  25850  pntibndlem2  25854  pntlemn  25863  pntlemj  25866  pntlemf  25868  pntlemo  25870  pntleml  25874  lnocoi  28230  nmlno0lem  28266  nmblolbii  28272  blocnilem  28277  blocni  28278  normcl  28598  occl  28777  hococli  29238  hosubcli  29242  hoaddcomi  29245  hodsi  29248  hoaddassi  29249  hocadddiri  29252  hocsubdiri  29253  ho2coi  29254  hoaddid1i  29259  ho0coi  29261  hoid1ri  29263  honegsubi  29269  ho01i  29301  ho02i  29302  dmadjrn  29368  nmopnegi  29438  lnopaddi  29444  lnopsubi  29447  hoddii  29462  nmlnop0iALT  29468  lnopmi  29473  lnophsi  29474  lnopcoi  29476  lnopeq0lem1  29478  lnopeqi  29481  lnopunilem1  29483  lnopunilem2  29484  lnophmlem2  29490  nmbdoplbi  29497  nmcopexi  29500  nmcoplbi  29501  nmophmi  29504  lnopconi  29507  lnfn0i  29515  lnfnaddi  29516  lnfnmuli  29517  lnfnsubi  29519  nmbdfnlbi  29522  nmcfnexi  29524  nmcfnlbi  29525  lnfnconi  29528  riesz3i  29535  riesz4i  29536  cnlnadjlem2  29541  cnlnadjlem4  29543  cnlnadjlem6  29545  cnlnadjlem7  29546  nmopadjlem  29562  nmoptrii  29567  nmopcoi  29568  adjcoi  29573  nmopcoadji  29574  bracnln  29582  opsqrlem5  29617  opsqrlem6  29618  hmopidmchi  29624  hmopidmpji  29625  pjsdii  29628  pjddii  29629  pjcohocli  29676  mhmhmeotmd  30792  xrge0pluscn  30805  voliune  31110  volfiniune  31111  ddemeas  31117  eulerpartlems  31240  eulerpartlemsv3  31241  eulerpartlemgc  31242  eulerpartlemgvv  31256  eulerpartlemgf  31259  eulerpartlemgs2  31260  eulerpartlemn  31261  derangen  32033  subfacf  32036  subfacp1lem6  32046  subfaclim  32049  subfacval3  32050  msrrcl  32404  msrid  32406  circum  32531  liminfval2  41616  ismbl3  41839  ovolsplit  41841  stirlinglem13  41939  fourierdlem55  42014  fourierdlem77  42036  fourierdlem80  42039