Theorem ffvelrni 3891

Description: A function's value belongs to its codomain.

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

Syntax hints:   -> wi 3   e. wcel 990  -->wf 3233  ` cfv 3237

This theorem is referenced by:  monoord 6415  uzrdgsuci 6597  ser1recli 6624  ser1monoi 6630  ser1add2i 6631  ser1addi 6632  ser0cl1i 6687  seq1bndi 7033  seq1ublem 7034  cau2i 7036  caubndi 7049  caurei 7050  cauimi 7051  ser1absdiflem 7052  serzrefi 7174  serzmulci 7181  climfnrcli 7234  clim2serzi 7268  climserzlei 7270  climubii 7276  climsupi 7278  climcaui 7279  caucvglem2 7281  caucvglem4 7283  caucvglem5 7284  caucvglem6 7285  caucvgi 7286  caucvg3ai 7287  caucvg3lem 7289  ser1f0i 7293  ser1cmpi 7297  ser1cmp2i 7300  cvgcmp2clem 7305  cvgcmpi 7307  cvgcmpubi 7308  cvgcmp3ci 7309  cvgcmp3cetlem1 7311  isumspliti 7339  geolimilem 7358  cvgratlem1ALT 7370  cvgratlem2ALT 7371  cvgratlem3ALT 7372  cvgratlem1 7373  cvgratlem2 7374  cvgratlem3 7375  cvgratlem4 7376  cvgratlem5 7377  negfcncfi 7392  abscncflem 7397  ivthlem8 7411  efsepi 7520  xplm 8095  bopcnlem4 8104  bcthlem28 8146  bcthlem30 8148  bcthlem33 8151  sqcn 8454  lnocoi 8537  nmlno0lem 8572  nmblolbii 8578  blocnilem 8583  blocni 8584  ubthlem3 8650  ubthlem5 8652  ubthlem9 8656  ubthlem11 8658  ubthlem12 8659  ubthlem13 8660  htthlem1 8739  htthlem6 8744  htthlem7 8745  sincolem 8783  effoi 8864  logcl 8877  relogcl 8878  normcl 9111  hlimcauii 9226  hlimuniii 9228  hococli 9811  hosubcli 9815  hoaddcomi 9818  hodsi 9821  hoaddassi 9822  hocadddiri 9825  hocsubdiri 9826  ho2coi 9827  hoaddid1i 9832  ho0coi 9834  hoid1ri 9836  honegsubi 9842  ho01i 9874  ho02i 9875  dmadjrn 9939  nmopnegi 10006  lnopaddi 10012  lnopsubi 10015  hoddii 10031  nmlnop0iALT 10037  lnopmi 10042  lnophsi 10043  lnopcoi 10045  lnopeq0lem1 10047  lnopeqi 10050  lnopunilem1 10052  lnopunilem2 10053  lnophmlem2 10059  nmbdoplbi 10066  nmcopexlem2 10069  nmcopexlem3 10070  nmcopexlem6 10073  nmcoplbi 10075  nmophmi 10078  lnopconi 10080  lnfn0i 10088  lnfnaddi 10089  lnfnmuli 10090  lnfnsubi 10092  nmbdfnlbi 10095  nmcfnexlem2 10098  nmcfnexlem3 10099  nmcfnexlem6 10102  nmcfnlbi 10104  lnfnconi 10107  nlelchi 10111  riesz3i 10112  riesz4i 10113  cnlnadjlem2 10118  cnlnadjlem6 10122  cnlnadjlem7 10123  nmopadjlem 10139  nmoptrii 10144  nmopcoi 10145  adjcoi 10150  nmopcoadji 10151  bracnln 10159  hmopidmchlem 10195  hmopidmchi 10196  hmopidmpji 10197  pjsdii 10200  pjddii 10201  pjcohocli 10249  ghomgrpilem2 10507

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832  ax-un 2920

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-uni 2552  df-br 2670  df-opab 2718  df-id 2889  df-xp 3239  df-cnv 3241  df-co 3242  df-dm 3243  df-rn 3244  df-res 3245  df-ima 3246  df-fun 3247  df-fn 3248  df-f 3249  df-fv 3253

Copyright terms: Public domain