Theorem ffvelrni 6036

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

Hypothesis

Ref	Expression
ffvrni.1	|- F : A --> B

Assertion

Ref	Expression
ffvelrni	|- ( C e. A -> ( F ` C ) e. B )

Proof of Theorem ffvelrni

Step	Hyp	Ref	Expression
1		ffvrni.1	. 2 |- F : A --> B
2		ffvelrn 6035	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3	1, 2	mpan 674	1 |- ( C e. A -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 1870   -->wf 5597   ` cfv 5601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609

This theorem is referenced by:  f0cli  6048  cantnfval2  8173  cantnfle  8175  cantnflt  8176  cantnfres  8181  cantnfp1lem3  8184  cantnflem1b  8190  cantnflem1d  8192  cantnflem1  8193  wemapwe  8201  cnfcomlem  8203  cnfcom  8204  cnfcom3lem  8207  cnfcom3  8208  ackbij1lem14  8661  ackbij1lem15  8662  ackbij1lem16  8663  ackbij1lem18  8665  fpwwe2lem8  9061  nqercl  9355  uzssz  11178  axdc4uzlem  12192  hashkf  12514  hashcl  12535  hashxrcl  12536  hashgadd  12553  cjcl  13147  limsupcl  13507  limsupclOLD  13508  limsuplt  13516  limsupltOLD  13517  limsupval2  13518  limsupval2OLD  13519  limsupgre  13520  limsupgreOLD  13521  limsupbnd2  13524  limsupbnd2OLD  13525  cn1lem  13639  climcn1lem  13644  caucvgrlem2  13718  fsumrelem  13845  ackbijnn  13864  efcl  14115  sincl  14158  coscl  14159  rpnnen2lem9  14253  rpnnen2  14256  sadcaddlem  14405  sadadd2lem  14407  sadadd3  14409  sadaddlem  14414  sadasslem  14418  sadeq  14420  algcvg  14506  algcvgb  14508  algcvga  14509  algfx  14510  eucalgcvga  14516  eucalg  14517  xpsaddlem  15432  xpsvsca  15436  xpsle  15438  efgtf  17307  efgtlen  17311  efginvrel2  17312  efginvrel1  17313  efgsp1  17322  efgredleme  17328  efgredlemc  17330  efgred  17333  efgred2  17338  efgcpbllemb  17340  frgpnabllem1  17444  xpsdsval  21327  xrhmeo  21870  ioorcl  22406  ioorclOLD  22411  volsup2  22440  volivth  22442  itg2const2  22576  itg2gt0  22595  dvcjbr  22780  dvcj  22781  dvfre  22782  rolle  22819  deg1xrcl  22908  plypf1  23034  resinf1o  23350  efif1olem4  23359  eff1olem  23362  logrncl  23382  relogcl  23390  asincl  23664  acoscl  23666  atancl  23672  asinrebnd  23692  dvatan  23726  leibpilem2  23732  leibpi  23733  areacl  23753  areage0  23754  divsqrtsumo1  23774  emcllem6  23791  emcllem7  23792  gamcl  23834  chtcl  23899  chpcl  23914  ppicl  23921  mucl  23931  sqff1o  23972  bposlem7  24081  dchrisum0lem2a  24218  mulog2sumlem1  24235  pntrsumo1  24266  pntrsumbnd  24267  pntrsumbnd2  24268  selbergr  24269  selberg3r  24270  selberg34r  24272  pntrlog2bndlem1  24278  pntrlog2bndlem2  24279  pntrlog2bndlem3  24280  pntrlog2bndlem4  24281  pntrlog2bndlem5  24282  pntrlog2bndlem6  24284  pntrlog2bnd  24285  pntpbnd1a  24286  pntpbnd1  24287  pntpbnd2  24288  pntibndlem2  24292  pntlemn  24301  pntlemj  24304  pntlemf  24306  pntlemo  24308  pntleml  24312  vdegp1ai  25557  lnocoi  26243  nmlno0lem  26279  nmblolbii  26285  blocnilem  26290  blocni  26291  normcl  26613  occl  26792  hococli  27253  hosubcli  27257  hoaddcomi  27260  hodsi  27263  hoaddassi  27264  hocadddiri  27267  hocsubdiri  27268  ho2coi  27269  hoaddid1i  27274  ho0coi  27276  hoid1ri  27278  honegsubi  27284  ho01i  27316  ho02i  27317  dmadjrn  27383  nmopnegi  27453  lnopaddi  27459  lnopsubi  27462  hoddii  27477  nmlnop0iALT  27483  lnopmi  27488  lnophsi  27489  lnopcoi  27491  lnopeq0lem1  27493  lnopeqi  27496  lnopunilem1  27498  lnopunilem2  27499  lnophmlem2  27505  nmbdoplbi  27512  nmcopexi  27515  nmcoplbi  27516  nmophmi  27519  lnopconi  27522  lnfn0i  27530  lnfnaddi  27531  lnfnmuli  27532  lnfnsubi  27534  nmbdfnlbi  27537  nmcfnexi  27539  nmcfnlbi  27540  lnfnconi  27543  riesz3i  27550  riesz4i  27551  cnlnadjlem2  27556  cnlnadjlem4  27558  cnlnadjlem6  27560  cnlnadjlem7  27561  nmopadjlem  27577  nmoptrii  27582  nmopcoi  27583  adjcoi  27588  nmopcoadji  27589  bracnln  27597  opsqrlem5  27632  opsqrlem6  27633  hmopidmchi  27639  hmopidmpji  27640  pjsdii  27643  pjddii  27644  pjcohocli  27691  mhmhmeotmd  28572  xrge0pluscn  28585  voliune  28891  volfiniune  28892  ddemeas  28898  eulerpartlems  29019  eulerpartlemsv3  29020  eulerpartlemgc  29021  eulerpartlemgvv  29035  eulerpartlemgf  29038  eulerpartlemgs2  29039  eulerpartlemn  29040  derangen  29683  subfacf  29686  subfacp1lem6  29696  subfaclim  29699  subfacval3  29700  msrrcl  29969  msrid  29971  ghomgrpilem2  30092  circum  30106  stirlinglem13  37517  fourierdlem55  37593  fourierdlem77  37615  fourierdlem80  37618