Theorem ffvelrni 6852

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

Syntax hints:   → wi 4   ∈ wcel 2114  ⟶wf 6353  ‘cfv 6357

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365

This theorem is referenced by:  f0cli  6866  cantnfval2  9134  cantnfle  9136  cantnflt  9137  cantnfres  9142  cantnfp1lem3  9145  cantnflem1b  9151  cantnflem1d  9153  cantnflem1  9154  wemapwe  9162  cnfcomlem  9164  cnfcom  9165  cnfcom3lem  9168  cnfcom3  9169  ackbij1lem14  9657  ackbij1lem15  9658  ackbij1lem16  9659  ackbij1lem18  9661  fpwwe2lem8  10061  nqercl  10355  uzssz  12267  axdc4uzlem  13354  hashkf  13695  hashcl  13720  hashxrcl  13721  hashgadd  13741  cjcl  14466  limsupcl  14832  limsuplt  14838  limsupval2  14839  limsupgre  14840  limsupbnd2  14842  cn1lem  14956  climcn1lem  14961  caucvgrlem2  15033  fsumrelem  15164  ackbijnn  15185  efcl  15438  sincl  15481  coscl  15482  rpnnen2lem9  15577  rpnnen2lem12  15580  sadcaddlem  15808  sadadd2lem  15810  sadadd3  15812  sadaddlem  15817  sadasslem  15821  sadeq  15823  algcvg  15922  algcvgb  15924  algcvga  15925  algfx  15926  eucalgcvga  15932  eucalg  15933  xpsaddlem  16848  xpsvsca  16852  xpsle  16854  efgtf  18850  efgtlen  18854  efginvrel2  18855  efginvrel1  18856  efgsp1  18865  efgredleme  18871  efgredlemc  18873  efgred  18876  efgred2  18881  efgcpbllemb  18883  frgpnabllem1  18995  xpsdsval  22993  xrhmeo  23552  ioorcl  24180  volsup2  24208  volivth  24210  itg2const2  24344  itg2gt0  24363  dvcjbr  24548  dvcj  24549  dvfre  24550  rolle  24589  deg1xrcl  24678  plypf1  24804  resinf1o  25122  efif1olem4  25131  eff1olem  25134  logrncl  25153  relogcl  25161  asincl  25453  acoscl  25455  atancl  25461  asinrebnd  25481  dvatan  25515  leibpilem2  25521  leibpi  25522  areacl  25542  areage0  25543  divsqrtsumo1  25563  emcllem6  25580  emcllem7  25581  gamcl  25623  chtcl  25688  chpcl  25703  ppicl  25710  mucl  25720  sqff1o  25761  bposlem7  25868  dchrisum0lem2a  26095  mulog2sumlem1  26112  pntrsumo1  26143  pntrsumbnd  26144  pntrsumbnd2  26145  selbergr  26146  selberg3r  26147  selberg34r  26149  pntrlog2bndlem1  26155  pntrlog2bndlem2  26156  pntrlog2bndlem3  26157  pntrlog2bndlem4  26158  pntrlog2bndlem5  26159  pntrlog2bndlem6  26161  pntrlog2bnd  26162  pntpbnd1a  26163  pntpbnd1  26164  pntpbnd2  26165  pntibndlem2  26169  pntlemn  26178  pntlemj  26181  pntlemf  26183  pntlemo  26185  pntleml  26189  lnocoi  28536  nmlno0lem  28572  nmblolbii  28578  blocnilem  28583  blocni  28584  normcl  28904  occl  29083  hococli  29544  hosubcli  29548  hoaddcomi  29551  hodsi  29554  hoaddassi  29555  hocadddiri  29558  hocsubdiri  29559  ho2coi  29560  hoaddid1i  29565  ho0coi  29567  hoid1ri  29569  honegsubi  29575  ho01i  29607  ho02i  29608  dmadjrn  29674  nmopnegi  29744  lnopaddi  29750  lnopsubi  29753  hoddii  29768  nmlnop0iALT  29774  lnopmi  29779  lnophsi  29780  lnopcoi  29782  lnopeq0lem1  29784  lnopeqi  29787  lnopunilem1  29789  lnopunilem2  29790  lnophmlem2  29796  nmbdoplbi  29803  nmcopexi  29806  nmcoplbi  29807  nmophmi  29810  lnopconi  29813  lnfn0i  29821  lnfnaddi  29822  lnfnmuli  29823  lnfnsubi  29825  nmbdfnlbi  29828  nmcfnexi  29830  nmcfnlbi  29831  lnfnconi  29834  riesz3i  29841  riesz4i  29842  cnlnadjlem2  29847  cnlnadjlem4  29849  cnlnadjlem6  29851  cnlnadjlem7  29852  nmopadjlem  29868  nmoptrii  29873  nmopcoi  29874  adjcoi  29879  nmopcoadji  29880  bracnln  29888  opsqrlem5  29923  opsqrlem6  29924  hmopidmchi  29930  hmopidmpji  29931  pjsdii  29934  pjddii  29935  pjcohocli  29982  mhmhmeotmd  31172  xrge0pluscn  31185  voliune  31490  volfiniune  31491  ddemeas  31497  eulerpartlems  31620  eulerpartlemsv3  31621  eulerpartlemgc  31622  eulerpartlemgvv  31636  eulerpartlemgf  31639  eulerpartlemgs2  31640  eulerpartlemn  31641  derangen  32421  subfacf  32424  subfacp1lem6  32434  subfaclim  32437  subfacval3  32438  msrrcl  32792  msrid  32794  circum  32919  liminfval2  42056  ismbl3  42278  ovolsplit  42280  stirlinglem13  42378  fourierdlem55  42453  fourierdlem77  42475  fourierdlem80  42478