Theorem ffvelrni 3821

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

Syntax hints:   -> wi 3   e. wcel 960  -->wf 3184  ` cfv 3188

This theorem is referenced by:  monoord 6295  uzrdgsuc 6305  ser1recl 6332  ser1mono 6338  ser1add2 6339  ser1add 6340  ser0cl1 6565  seq1bnd 6910  seq1ublem 6911  cau2 6913  caubnd 6926  caure 6927  cauim 6928  ser1absdiflem 6929  serzref 7051  serzmulc 7058  climfnrcl 7111  clim2serz 7145  climserzle 7147  climubi 7153  climsup 7155  climcau 7156  caucvglem2 7158  caucvglem4 7160  caucvglem5 7161  caucvglem6 7162  caucvg 7163  caucvg3a 7164  caucvg3lem 7166  ser1f0 7170  ser1cmp 7174  ser1cmp2 7177  cvgcmp2clem 7182  cvgcmp 7184  cvgcmpub 7185  cvgcmp3c 7186  cvgcmp3cetlem1 7188  isumsplit 7216  geolimilem 7235  cvgratlem1ALT 7247  cvgratlem2ALT 7248  cvgratlem3ALT 7249  cvgratlem1 7250  cvgratlem2 7251  cvgratlem3 7252  cvgratlem4 7253  cvgratlem5 7254  negfcncf 7269  abscncflem 7274  ivthlem8 7288  efsep 7396  xplm 7972  bopcnlem4 7981  bcthlem28 8023  bcthlem30 8025  bcthlem33 8028  sqcn 8331  lnocoi 8414  nmlno0lem 8449  nmblolbii 8455  blocnilem 8460  blocni 8461  ubthlem3 8527  ubthlem5 8529  ubthlem9 8533  ubthlem11 8535  ubthlem12 8536  ubthlem13 8537  htthlem1 8616  htthlem6 8621  htthlem7 8622  sincolem 8660  effoi 8740  logclt 8753  relogclt 8754  normclt 8986  hlimcaui 9101  hlimunii 9103  hococl 9686  hosubcl 9690  hoaddcom 9693  hods 9696  hoaddass 9697  hocadddir 9700  hocsubdir 9701  ho2co 9702  hoaddid1 9707  ho0co 9709  hoid1r 9711  honegsub 9717  ho01 9749  ho02 9750  dmadjrnt 9816  nmopneg 9884  lnopadd 9890  lnopsub 9893  hoddi 9909  nmlnop0ALT 9915  lnopm 9920  lnophs 9921  lnopco 9923  lnopeq0lem1 9925  lnopeq 9928  lnopunilem1 9930  lnopunilem2 9931  lnophmlem2 9937  nmbdoplb 9944  nmcopexlem2 9947  nmcopexlem3 9948  nmcopexlem6 9951  nmcoplb 9953  nmophm 9956  lnopcon 9958  lnfn0 9966  lnfnadd 9967  lnfnmul 9968  lnfnsub 9970  nmbdfnlb 9973  nmcfnexlem2 9976  nmcfnexlem3 9977  nmcfnexlem6 9980  nmcfnlb 9982  lnfncon 9985  nlelch 9989  riesz3 9990  riesz4 9991  cnlnadjlem2 9996  cnlnadjlem6 10000  cnlnadjlem7 10001  nmopadjlem 10017  nmoptri 10022  nmopco 10023  adjco 10028  nmopcoadj 10029  bracnlnt 10037  hmopidmchlem 10073  hmopidmch 10074  hmopidmpj 10075  pjsdi 10078  pjddi 10079  pjcohocl 10126  ghomgrpilem2 10381

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-rex 1653  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-id 2841  df-xp 3190  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-fv 3204

Copyright terms: Public domain