Theorem ffvelrni 5837

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 5836	. 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 1756   -->wf 5409   ` cfv 5413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421

This theorem is referenced by:  f0cli  5849  cantnfval2  7869  cantnfle  7871  cantnflt  7872  cantnfres  7877  cantnfp1lem3  7880  cantnflem1b  7886  cantnflem1d  7888  cantnflem1  7889  cantnfval2OLD  7899  cantnfleOLD  7901  cantnfltOLD  7902  cantnfp1lem3OLD  7906  cantnflem1bOLD  7909  cantnflem1dOLD  7911  cantnflem1OLD  7912  wemapwe  7920  wemapweOLD  7921  cnfcomlem  7924  cnfcom  7925  cnfcom3lem  7928  cnfcom3  7929  cnfcomlemOLD  7932  cnfcomOLD  7933  cnfcom3lemOLD  7936  cnfcom3OLD  7937  ackbij1lem14  8394  ackbij1lem15  8395  ackbij1lem16  8396  ackbij1lem18  8398  fpwwe2lem8  8796  nqercl  9092  uzssz  10872  axdc4uzlem  11796  hashkf  12097  hashcl  12118  hashxrcl  12119  hashgadd  12132  cjcl  12586  limsupcl  12943  limsuplt  12949  limsupval2  12950  limsupgre  12951  limsupbnd2  12953  cn1lem  13067  climcn1lem  13072  caucvgrlem2  13144  fsumrelem  13262  ackbijnn  13283  efcl  13360  sincl  13402  coscl  13403  rpnnen2lem9  13497  rpnnen2  13500  sadcaddlem  13645  sadadd2lem  13647  sadadd3  13649  sadaddlem  13654  sadasslem  13658  sadeq  13660  algcvg  13743  algcvgb  13745  algcvga  13746  algfx  13747  eucalgcvga  13753  eucalg  13754  xpsaddlem  14505  xpsvsca  14509  xpsle  14511  efgtf  16210  efgtlen  16214  efginvrel2  16215  efginvrel1  16216  efgsp1  16225  efgredleme  16231  efgredlemc  16233  efgred  16236  efgred2  16241  efgcpbllemb  16243  frgpnabllem1  16342  xpsdsval  19931  xrhmeo  20493  ioorcl  21032  volsup2  21060  volivth  21062  itg2const2  21194  itg2gt0  21213  dvcjbr  21398  dvcj  21399  dvfre  21400  rolle  21437  deg1xrcl  21528  plypf1  21655  resinf1o  21967  efif1olem4  21976  eff1olem  21979  logrncl  21994  relogcl  22002  asincl  22243  acoscl  22245  atancl  22251  asinrebnd  22271  dvatan  22305  leibpilem2  22311  leibpi  22312  areacl  22331  areage0  22332  divsqrsumo1  22352  emcllem6  22369  emcllem7  22370  chtcl  22422  chpcl  22437  ppicl  22444  mucl  22454  sqff1o  22495  bposlem7  22604  dchrisum0lem2a  22741  mulog2sumlem1  22758  pntrsumo1  22789  pntrsumbnd  22790  pntrsumbnd2  22791  selbergr  22792  selberg3r  22793  selberg34r  22795  pntrlog2bndlem1  22801  pntrlog2bndlem2  22802  pntrlog2bndlem3  22803  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntrlog2bnd  22808  pntpbnd1a  22809  pntpbnd1  22810  pntpbnd2  22811  pntibndlem2  22815  pntlemn  22824  pntlemj  22827  pntlemf  22829  pntlemo  22831  pntleml  22835  vdegp1ai  23556  lnocoi  24108  nmlno0lem  24144  nmblolbii  24150  blocnilem  24155  blocni  24156  normcl  24478  occl  24658  hococli  25120  hosubcli  25124  hoaddcomi  25127  hodsi  25130  hoaddassi  25131  hocadddiri  25134  hocsubdiri  25135  ho2coi  25136  hoaddid1i  25141  ho0coi  25143  hoid1ri  25145  honegsubi  25151  ho01i  25183  ho02i  25184  dmadjrn  25250  nmopnegi  25320  lnopaddi  25326  lnopsubi  25329  hoddii  25344  nmlnop0iALT  25350  lnopmi  25355  lnophsi  25356  lnopcoi  25358  lnopeq0lem1  25360  lnopeqi  25363  lnopunilem1  25365  lnopunilem2  25366  lnophmlem2  25372  nmbdoplbi  25379  nmcopexi  25382  nmcoplbi  25383  nmophmi  25386  lnopconi  25389  lnfn0i  25397  lnfnaddi  25398  lnfnmuli  25399  lnfnsubi  25401  nmbdfnlbi  25404  nmcfnexi  25406  nmcfnlbi  25407  lnfnconi  25410  riesz3i  25417  riesz4i  25418  cnlnadjlem2  25423  cnlnadjlem4  25425  cnlnadjlem6  25427  cnlnadjlem7  25428  nmopadjlem  25444  nmoptrii  25449  nmopcoi  25450  adjcoi  25455  nmopcoadji  25456  bracnln  25464  opsqrlem5  25499  opsqrlem6  25500  hmopidmchi  25506  hmopidmpji  25507  pjsdii  25510  pjddii  25511  pjcohocli  25558  mhmhmeotmd  26309  xrge0pluscn  26322  voliune  26597  volfiniune  26598  ddemeas  26604  eulerpartlems  26695  eulerpartlemsv3  26696  eulerpartlemgc  26697  eulerpartlemgvv  26711  eulerpartlemgf  26714  eulerpartlemgs2  26715  eulerpartlemn  26716  gamcl  26982  derangen  27012  subfacf  27015  subfacp1lem6  27025  subfaclim  27028  subfacval3  27029  ghomgrpilem2  27256  circum  27270  stirlinglem13  29834