Theorem ffvelrni 6020

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 6019	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3	1, 2	mpan 670	1 |- ( C e. A -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 1767   -->wf 5584   ` cfv 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-fv 5596

This theorem is referenced by:  f0cli  6032  cantnfval2  8088  cantnfle  8090  cantnflt  8091  cantnfres  8096  cantnfp1lem3  8099  cantnflem1b  8105  cantnflem1d  8107  cantnflem1  8108  cantnfval2OLD  8118  cantnfleOLD  8120  cantnfltOLD  8121  cantnfp1lem3OLD  8125  cantnflem1bOLD  8128  cantnflem1dOLD  8130  cantnflem1OLD  8131  wemapwe  8139  wemapweOLD  8140  cnfcomlem  8143  cnfcom  8144  cnfcom3lem  8147  cnfcom3  8148  cnfcomlemOLD  8151  cnfcomOLD  8152  cnfcom3lemOLD  8155  cnfcom3OLD  8156  ackbij1lem14  8613  ackbij1lem15  8614  ackbij1lem16  8615  ackbij1lem18  8617  fpwwe2lem8  9015  nqercl  9309  uzssz  11101  axdc4uzlem  12060  hashkf  12375  hashcl  12396  hashxrcl  12397  hashgadd  12413  cjcl  12901  limsupcl  13259  limsuplt  13265  limsupval2  13266  limsupgre  13267  limsupbnd2  13269  cn1lem  13383  climcn1lem  13388  caucvgrlem2  13460  fsumrelem  13584  ackbijnn  13603  efcl  13680  sincl  13722  coscl  13723  rpnnen2lem9  13817  rpnnen2  13820  sadcaddlem  13966  sadadd2lem  13968  sadadd3  13970  sadaddlem  13975  sadasslem  13979  sadeq  13981  algcvg  14064  algcvgb  14066  algcvga  14067  algfx  14068  eucalgcvga  14074  eucalg  14075  xpsaddlem  14830  xpsvsca  14834  xpsle  14836  efgtf  16546  efgtlen  16550  efginvrel2  16551  efginvrel1  16552  efgsp1  16561  efgredleme  16567  efgredlemc  16569  efgred  16572  efgred2  16577  efgcpbllemb  16579  frgpnabllem1  16680  xpsdsval  20647  xrhmeo  21209  ioorcl  21749  volsup2  21777  volivth  21779  itg2const2  21911  itg2gt0  21930  dvcjbr  22115  dvcj  22116  dvfre  22117  rolle  22154  deg1xrcl  22245  plypf1  22372  resinf1o  22684  efif1olem4  22693  eff1olem  22696  logrncl  22711  relogcl  22719  asincl  22960  acoscl  22962  atancl  22968  asinrebnd  22988  dvatan  23022  leibpilem2  23028  leibpi  23029  areacl  23048  areage0  23049  divsqrtsumo1  23069  emcllem6  23086  emcllem7  23087  chtcl  23139  chpcl  23154  ppicl  23161  mucl  23171  sqff1o  23212  bposlem7  23321  dchrisum0lem2a  23458  mulog2sumlem1  23475  pntrsumo1  23506  pntrsumbnd  23507  pntrsumbnd2  23508  selbergr  23509  selberg3r  23510  selberg34r  23512  pntrlog2bndlem1  23518  pntrlog2bndlem2  23519  pntrlog2bndlem3  23520  pntrlog2bndlem4  23521  pntrlog2bndlem5  23522  pntrlog2bndlem6  23524  pntrlog2bnd  23525  pntpbnd1a  23526  pntpbnd1  23527  pntpbnd2  23528  pntibndlem2  23532  pntlemn  23541  pntlemj  23544  pntlemf  23546  pntlemo  23548  pntleml  23552  vdegp1ai  24688  lnocoi  25376  nmlno0lem  25412  nmblolbii  25418  blocnilem  25423  blocni  25424  normcl  25746  occl  25926  hococli  26388  hosubcli  26392  hoaddcomi  26395  hodsi  26398  hoaddassi  26399  hocadddiri  26402  hocsubdiri  26403  ho2coi  26404  hoaddid1i  26409  ho0coi  26411  hoid1ri  26413  honegsubi  26419  ho01i  26451  ho02i  26452  dmadjrn  26518  nmopnegi  26588  lnopaddi  26594  lnopsubi  26597  hoddii  26612  nmlnop0iALT  26618  lnopmi  26623  lnophsi  26624  lnopcoi  26626  lnopeq0lem1  26628  lnopeqi  26631  lnopunilem1  26633  lnopunilem2  26634  lnophmlem2  26640  nmbdoplbi  26647  nmcopexi  26650  nmcoplbi  26651  nmophmi  26654  lnopconi  26657  lnfn0i  26665  lnfnaddi  26666  lnfnmuli  26667  lnfnsubi  26669  nmbdfnlbi  26672  nmcfnexi  26674  nmcfnlbi  26675  lnfnconi  26678  riesz3i  26685  riesz4i  26686  cnlnadjlem2  26691  cnlnadjlem4  26693  cnlnadjlem6  26695  cnlnadjlem7  26696  nmopadjlem  26712  nmoptrii  26717  nmopcoi  26718  adjcoi  26723  nmopcoadji  26724  bracnln  26732  opsqrlem5  26767  opsqrlem6  26768  hmopidmchi  26774  hmopidmpji  26775  pjsdii  26778  pjddii  26779  pjcohocli  26826  mhmhmeotmd  27573  xrge0pluscn  27586  voliune  27869  volfiniune  27870  ddemeas  27876  eulerpartlems  27967  eulerpartlemsv3  27968  eulerpartlemgc  27969  eulerpartlemgvv  27983  eulerpartlemgf  27986  eulerpartlemgs2  27987  eulerpartlemn  27988  gamcl  28254  derangen  28284  subfacf  28287  subfacp1lem6  28297  subfaclim  28300  subfacval3  28301  ghomgrpilem2  28529  circum  28543  stirlinglem13  31414  fourierdlem77  31512  fourierdlem80  31515