Theorem ffvelrni 6358

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

Syntax hints:   -> wi 4   e. wcel 1990   -->wf 5884   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  f0cli  6370  cantnfval2  8566  cantnfle  8568  cantnflt  8569  cantnfres  8574  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1d  8585  cantnflem1  8586  wemapwe  8594  cnfcomlem  8596  cnfcom  8597  cnfcom3lem  8600  cnfcom3  8601  ackbij1lem14  9055  ackbij1lem15  9056  ackbij1lem16  9057  ackbij1lem18  9059  fpwwe2lem8  9459  nqercl  9753  uzssz  11707  axdc4uzlem  12782  hashkf  13119  hashcl  13147  hashxrcl  13148  hashgadd  13166  cjcl  13845  limsupcl  14204  limsuplt  14210  limsupval2  14211  limsupgre  14212  limsupbnd2  14214  cn1lem  14328  climcn1lem  14333  caucvgrlem2  14405  fsumrelem  14539  ackbijnn  14560  efcl  14813  sincl  14856  coscl  14857  rpnnen2lem9  14951  rpnnen2lem12  14954  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  sadaddlem  15188  sadasslem  15192  sadeq  15194  algcvg  15289  algcvgb  15291  algcvga  15292  algfx  15293  eucalgcvga  15299  eucalg  15300  xpsaddlem  16235  xpsvsca  16239  xpsle  16241  efgtf  18135  efgtlen  18139  efginvrel2  18140  efginvrel1  18141  efgsp1  18150  efgredleme  18156  efgredlemc  18158  efgred  18161  efgred2  18166  efgcpbllemb  18168  frgpnabllem1  18276  xpsdsval  22186  xrhmeo  22745  ioorcl  23345  volsup2  23373  volivth  23375  itg2const2  23508  itg2gt0  23527  dvcjbr  23712  dvcj  23713  dvfre  23714  rolle  23753  deg1xrcl  23842  plypf1  23968  resinf1o  24282  efif1olem4  24291  eff1olem  24294  logrncl  24314  relogcl  24322  asincl  24600  acoscl  24602  atancl  24608  asinrebnd  24628  dvatan  24662  leibpilem2  24668  leibpi  24669  areacl  24689  areage0  24690  divsqrtsumo1  24710  emcllem6  24727  emcllem7  24728  gamcl  24770  chtcl  24835  chpcl  24850  ppicl  24857  mucl  24867  sqff1o  24908  bposlem7  25015  dchrisum0lem2a  25206  mulog2sumlem1  25223  pntrsumo1  25254  pntrsumbnd  25255  pntrsumbnd2  25256  selbergr  25257  selberg3r  25258  selberg34r  25260  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntlemn  25289  pntlemj  25292  pntlemf  25294  pntlemo  25296  pntleml  25300  lnocoi  27612  nmlno0lem  27648  nmblolbii  27654  blocnilem  27659  blocni  27660  normcl  27982  occl  28163  hococli  28624  hosubcli  28628  hoaddcomi  28631  hodsi  28634  hoaddassi  28635  hocadddiri  28638  hocsubdiri  28639  ho2coi  28640  hoaddid1i  28645  ho0coi  28647  hoid1ri  28649  honegsubi  28655  ho01i  28687  ho02i  28688  dmadjrn  28754  nmopnegi  28824  lnopaddi  28830  lnopsubi  28833  hoddii  28848  nmlnop0iALT  28854  lnopmi  28859  lnophsi  28860  lnopcoi  28862  lnopeq0lem1  28864  lnopeqi  28867  lnopunilem1  28869  lnopunilem2  28870  lnophmlem2  28876  nmbdoplbi  28883  nmcopexi  28886  nmcoplbi  28887  nmophmi  28890  lnopconi  28893  lnfn0i  28901  lnfnaddi  28902  lnfnmuli  28903  lnfnsubi  28905  nmbdfnlbi  28908  nmcfnexi  28910  nmcfnlbi  28911  lnfnconi  28914  riesz3i  28921  riesz4i  28922  cnlnadjlem2  28927  cnlnadjlem4  28929  cnlnadjlem6  28931  cnlnadjlem7  28932  nmopadjlem  28948  nmoptrii  28953  nmopcoi  28954  adjcoi  28959  nmopcoadji  28960  bracnln  28968  opsqrlem5  29003  opsqrlem6  29004  hmopidmchi  29010  hmopidmpji  29011  pjsdii  29014  pjddii  29015  pjcohocli  29062  mhmhmeotmd  29973  xrge0pluscn  29986  voliune  30292  volfiniune  30293  ddemeas  30299  eulerpartlems  30422  eulerpartlemsv3  30423  eulerpartlemgc  30424  eulerpartlemgvv  30438  eulerpartlemgf  30441  eulerpartlemgs2  30442  eulerpartlemn  30443  derangen  31154  subfacf  31157  subfacp1lem6  31167  subfaclim  31170  subfacval3  31171  msrrcl  31440  msrid  31442  circum  31568  liminfval2  40000  ismbl3  40203  ovolsplit  40205  stirlinglem13  40303  fourierdlem55  40378  fourierdlem77  40400  fourierdlem80  40403