Theorem ffvelcdmi 7031

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 7029	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 696	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500

This theorem is referenced by:  f0cli  7046  cantnfval2  9588  cantnfle  9590  cantnflt  9591  cantnfres  9596  cantnfp1lem3  9599  cantnflem1b  9605  cantnflem1d  9607  cantnflem1  9608  wemapwe  9616  cnfcomlem  9618  cnfcom  9619  cnfcom3lem  9622  cnfcom3  9623  ackbij1lem14  10152  ackbij1lem15  10153  ackbij1lem16  10154  ackbij1lem18  10156  fpwwe2lem7  10558  nqercl  10852  uzssz  12807  axdc4uzlem  13943  hashkf  14292  hashcl  14316  hashxrcl  14317  hashgadd  14337  cjcl  15065  limsupcl  15433  limsuplt  15439  limsupval2  15440  limsupgre  15441  limsupbnd2  15443  cn1lem  15558  climcn1lem  15563  caucvgrlem2  15635  fsumrelem  15768  ackbijnn  15791  efcl  16045  sincl  16091  coscl  16092  rpnnen2lem9  16187  rpnnen2lem12  16190  sadcaddlem  16424  sadadd2lem  16426  sadadd3  16428  sadaddlem  16433  sadasslem  16437  sadeq  16439  algcvg  16543  algcvgb  16545  algcvga  16546  algfx  16547  eucalgcvga  16553  eucalg  16554  xpsaddlem  17535  xpsvsca  17539  xpsle  17541  efgtf  19695  efgtlen  19699  efginvrel2  19700  efginvrel1  19701  efgsp1  19710  efgredleme  19716  efgredlemc  19718  efgred  19721  efgred2  19726  efgcpbllemb  19728  frgpnabllem1  19846  xpsdsval  24371  xrhmeo  24938  ioorcl  25569  volsup2  25597  volivth  25599  itg2const2  25733  itg2gt0  25752  dvcjbr  25941  dvcj  25942  dvfre  25943  rolle  25982  deg1xrcl  26072  plypf1  26202  resinf1o  26525  efif1olem4  26534  eff1olem  26537  logrncl  26556  relogcl  26564  asincl  26862  acoscl  26864  atancl  26870  asinrebnd  26890  dvatan  26924  leibpilem2  26930  leibpi  26931  areacl  26951  areage0  26952  divsqrtsumo1  26972  emcllem6  26989  emcllem7  26990  gamcl  27032  chtcl  27097  chpcl  27112  ppicl  27119  mucl  27129  sqff1o  27170  bposlem7  27278  dchrisum0lem2a  27505  mulog2sumlem1  27522  pntrsumo1  27553  pntrsumbnd  27554  pntrsumbnd2  27555  selbergr  27556  selberg3r  27557  selberg34r  27559  pntrlog2bndlem1  27565  pntrlog2bndlem2  27566  pntrlog2bndlem3  27567  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntrlog2bndlem6  27571  pntrlog2bnd  27572  pntpbnd1a  27573  pntpbnd1  27574  pntpbnd2  27575  pntibndlem2  27579  pntlemn  27588  pntlemj  27591  pntlemf  27593  pntlemo  27595  pntleml  27599  newf  27855  leftf  27872  rightf  27873  elmade  27874  sltsleft  27877  sltsright  27878  lnocoi  30853  nmlno0lem  30889  nmblolbii  30895  blocnilem  30900  blocni  30901  normcl  31221  occl  31400  hococli  31861  hosubcli  31865  hoaddcomi  31868  hodsi  31871  hoaddassi  31872  hocadddiri  31875  hocsubdiri  31876  ho2coi  31877  hoaddridi  31882  ho0coi  31884  hoid1ri  31886  honegsubi  31892  ho01i  31924  ho02i  31925  dmadjrn  31991  nmopnegi  32061  lnopaddi  32067  lnopsubi  32070  hoddii  32085  nmlnop0iALT  32091  lnopmi  32096  lnophsi  32097  lnopcoi  32099  lnopeq0lem1  32101  lnopeqi  32104  lnopunilem1  32106  lnopunilem2  32107  lnophmlem2  32113  nmbdoplbi  32120  nmcopexi  32123  nmcoplbi  32124  nmophmi  32127  lnopconi  32130  lnfn0i  32138  lnfnaddi  32139  lnfnmuli  32140  lnfnsubi  32142  nmbdfnlbi  32145  nmcfnexi  32147  nmcfnlbi  32148  lnfnconi  32151  riesz3i  32158  riesz4i  32159  cnlnadjlem2  32164  cnlnadjlem4  32166  cnlnadjlem6  32168  cnlnadjlem7  32169  nmopadjlem  32185  nmoptrii  32190  nmopcoi  32191  adjcoi  32196  nmopcoadji  32197  bracnln  32205  opsqrlem5  32240  opsqrlem6  32241  hmopidmchi  32247  hmopidmpji  32248  pjsdii  32251  pjddii  32252  pjcohocli  32299  mhmhmeotmd  34118  xrge0pluscn  34131  voliune  34420  volfiniune  34421  ddemeas  34427  eulerpartlems  34551  eulerpartlemsv3  34552  eulerpartlemgc  34553  eulerpartlemgvv  34567  eulerpartlemgf  34570  eulerpartlemgs2  34571  eulerpartlemn  34572  derangen  35407  subfacf  35410  subfacp1lem6  35420  subfaclim  35423  subfacval3  35424  msrrcl  35778  msrid  35780  circum  35909  fpwfvss  43863  liminfval2  46218  ismbl3  46436  ovolsplit  46438  stirlinglem13  46536  fourierdlem55  46611  fourierdlem77  46633  fourierdlem80  46636