Theorem ffvelcdmi 7029

Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)

Hypothesis

Ref	Expression
ffvelcdmi.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

Ref	Expression
ffvelcdmi	⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdmi

Step	Hyp	Ref	Expression
1		ffvelcdmi.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		ffvelcdm 7027	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 691	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2114  ⟶wf 6488  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  f0cli  7044  cantnfval2  9581  cantnfle  9583  cantnflt  9584  cantnfres  9589  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1d  9600  cantnflem1  9601  wemapwe  9609  cnfcomlem  9611  cnfcom  9612  cnfcom3lem  9615  cnfcom3  9616  ackbij1lem14  10145  ackbij1lem15  10146  ackbij1lem16  10147  ackbij1lem18  10149  fpwwe2lem7  10551  nqercl  10845  uzssz  12800  axdc4uzlem  13936  hashkf  14285  hashcl  14309  hashxrcl  14310  hashgadd  14330  cjcl  15058  limsupcl  15426  limsuplt  15432  limsupval2  15433  limsupgre  15434  limsupbnd2  15436  cn1lem  15551  climcn1lem  15556  caucvgrlem2  15628  fsumrelem  15761  ackbijnn  15784  efcl  16038  sincl  16084  coscl  16085  rpnnen2lem9  16180  rpnnen2lem12  16183  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  sadaddlem  16426  sadasslem  16430  sadeq  16432  algcvg  16536  algcvgb  16538  algcvga  16539  algfx  16540  eucalgcvga  16546  eucalg  16547  xpsaddlem  17528  xpsvsca  17532  xpsle  17534  efgtf  19688  efgtlen  19692  efginvrel2  19693  efginvrel1  19694  efgsp1  19703  efgredleme  19709  efgredlemc  19711  efgred  19714  efgred2  19719  efgcpbllemb  19721  frgpnabllem1  19839  xpsdsval  24356  xrhmeo  24923  ioorcl  25554  volsup2  25582  volivth  25584  itg2const2  25718  itg2gt0  25737  dvcjbr  25926  dvcj  25927  dvfre  25928  rolle  25967  deg1xrcl  26057  plypf1  26187  resinf1o  26513  efif1olem4  26522  eff1olem  26525  logrncl  26544  relogcl  26552  asincl  26850  acoscl  26852  atancl  26858  asinrebnd  26878  dvatan  26912  leibpilem2  26918  leibpi  26919  areacl  26939  areage0  26940  divsqrtsumo1  26961  emcllem6  26978  emcllem7  26979  gamcl  27021  chtcl  27086  chpcl  27101  ppicl  27108  mucl  27118  sqff1o  27159  bposlem7  27267  dchrisum0lem2a  27494  mulog2sumlem1  27511  pntrsumo1  27542  pntrsumbnd  27543  pntrsumbnd2  27544  selbergr  27545  selberg3r  27546  selberg34r  27548  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntrlog2bnd  27561  pntpbnd1a  27562  pntpbnd1  27563  pntpbnd2  27564  pntibndlem2  27568  pntlemn  27577  pntlemj  27580  pntlemf  27582  pntlemo  27584  pntleml  27588  newf  27844  leftf  27861  rightf  27862  elmade  27863  sltsleft  27866  sltsright  27867  lnocoi  30843  nmlno0lem  30879  nmblolbii  30885  blocnilem  30890  blocni  30891  normcl  31211  occl  31390  hococli  31851  hosubcli  31855  hoaddcomi  31858  hodsi  31861  hoaddassi  31862  hocadddiri  31865  hocsubdiri  31866  ho2coi  31867  hoaddridi  31872  ho0coi  31874  hoid1ri  31876  honegsubi  31882  ho01i  31914  ho02i  31915  dmadjrn  31981  nmopnegi  32051  lnopaddi  32057  lnopsubi  32060  hoddii  32075  nmlnop0iALT  32081  lnopmi  32086  lnophsi  32087  lnopcoi  32089  lnopeq0lem1  32091  lnopeqi  32094  lnopunilem1  32096  lnopunilem2  32097  lnophmlem2  32103  nmbdoplbi  32110  nmcopexi  32113  nmcoplbi  32114  nmophmi  32117  lnopconi  32120  lnfn0i  32128  lnfnaddi  32129  lnfnmuli  32130  lnfnsubi  32132  nmbdfnlbi  32135  nmcfnexi  32137  nmcfnlbi  32138  lnfnconi  32141  riesz3i  32148  riesz4i  32149  cnlnadjlem2  32154  cnlnadjlem4  32156  cnlnadjlem6  32158  cnlnadjlem7  32159  nmopadjlem  32175  nmoptrii  32180  nmopcoi  32181  adjcoi  32186  nmopcoadji  32187  bracnln  32195  opsqrlem5  32230  opsqrlem6  32231  hmopidmchi  32237  hmopidmpji  32238  pjsdii  32241  pjddii  32242  pjcohocli  32289  mhmhmeotmd  34087  xrge0pluscn  34100  voliune  34389  volfiniune  34390  ddemeas  34396  eulerpartlems  34520  eulerpartlemsv3  34521  eulerpartlemgc  34522  eulerpartlemgvv  34536  eulerpartlemgf  34539  eulerpartlemgs2  34540  eulerpartlemn  34541  derangen  35370  subfacf  35373  subfacp1lem6  35383  subfaclim  35386  subfacval3  35387  msrrcl  35741  msrid  35743  circum  35872  fpwfvss  43857  liminfval2  46214  ismbl3  46432  ovolsplit  46434  stirlinglem13  46532  fourierdlem55  46607  fourierdlem77  46629  fourierdlem80  46632