Theorem ffvelrni 3806

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

Syntax hints:   -> wi 3   e. wcel 956  -->wf 3173  ` cfv 3177

This theorem is referenced by:  monoord 6239  uzrdgsuc 6249  ser1recl 6276  ser1mono 6282  ser1add2 6283  ser1add 6284  ser0cl1 6504  seq1bnd 6855  seq1ublem 6856  cau2 6858  caubnd 6871  caure 6872  cauim 6873  ser1absdiflem 6874  serzref 6997  serzmulc 7004  climfnrcl 7056  clim2serz 7089  climserzle 7091  climubi 7097  climsup 7099  climcau 7100  caucvglem2 7102  caucvglem4 7104  caucvglem5 7105  caucvglem6 7106  caucvg 7107  caucvg3a 7108  caucvg3lem 7110  ser1f0 7114  ser1cmp 7118  ser1cmp2 7121  cvgcmp2clem 7126  cvgcmp 7128  cvgcmpub 7129  cvgcmp3c 7130  cvgcmp3cetlem1 7132  isumsplit 7159  geolimilem 7178  cvgratlem1ALT 7190  cvgratlem2ALT 7191  cvgratlem3ALT 7192  cvgratlem1 7193  cvgratlem2 7194  cvgratlem3 7195  cvgratlem4 7196  cvgratlem5 7197  negfcncf 7212  abscncflem 7217  ivthlem8 7231  ivthlem4OLD 7236  ivthlem6OLD 7238  ivthlem7OLD 7239  ivthlem8OLD 7240  efsep 7345  xplm 7925  bopcnlem4 7934  bcthlem28 7976  bcthlem30 7978  bcthlem33 7981  sqcn 8283  lnocoi 8365  nmlno0lem 8398  nmblolbii 8403  blocnilem 8408  blocni 8409  ubthlem3 8475  ubthlem5 8477  ubthlem9 8481  ubthlem11 8483  ubthlem12 8484  ubthlem13 8485  htthlem1 8563  htthlem6 8568  htthlem7 8569  sincolem 8603  effoi 8684  logclt 8697  relogclt 8698  normclt 8930  hlimcaui 9045  hlimunii 9047  hococl 9631  hosubcl 9635  hoaddcom 9638  hods 9641  hoaddass 9642  hocadddir 9645  hocsubdir 9646  ho2co 9647  hoaddid1 9652  ho0co 9654  hoid1r 9656  honegsub 9662  ho01 9694  ho02 9695  dmadjrnt 9761  nmopneg 9828  lnopadd 9834  lnopsub 9837  hoddi 9852  nmlnop0ALT 9858  lnopm 9863  lnophs 9864  lnopco 9866  lnopeq0lem1 9868  lnopeq 9871  lnopunilem1 9873  lnopunilem2 9874  lnophmlem2 9880  nmbdoplb 9887  nmcopexlem2 9890  nmcopexlem3 9891  nmcopexlem6 9894  nmcoplb 9896  nmophm 9899  lnopcon 9901  lnfn0 9909  lnfnadd 9910  lnfnmul 9911  lnfnsub 9913  nmbdfnlb 9916  nmcfnexlem2 9919  nmcfnexlem3 9920  nmcfnexlem6 9923  nmcfnlb 9925  lnfncon 9928  nlelch 9932  riesz3 9933  riesz4 9934  cnlnadjlem2 9939  cnlnadjlem6 9943  cnlnadjlem7 9944  nmopadjlem 9960  nmoptri 9965  nmopco 9966  adjco 9971  nmopcoadj 9972  bracnlnt 9980  hmopidmchlem 10016  hmopidmch 10017  hmopidmpj 10018  pjsdi 10021  pjddi 10022  pjcohocl 10069  ghomgrpilem2 10320

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-id 2830  df-xp 3179  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-fv 3193

Copyright terms: Public domain