Theorem ffvelcdmi 7055

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

Syntax hints:   → wi 4   ∈ wcel 2109  ⟶wf 6507  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  f0cli  7070  cantnfval2  9622  cantnfle  9624  cantnflt  9625  cantnfres  9630  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1d  9641  cantnflem1  9642  wemapwe  9650  cnfcomlem  9652  cnfcom  9653  cnfcom3lem  9656  cnfcom3  9657  ackbij1lem14  10185  ackbij1lem15  10186  ackbij1lem16  10187  ackbij1lem18  10189  fpwwe2lem7  10590  nqercl  10884  uzssz  12814  axdc4uzlem  13948  hashkf  14297  hashcl  14321  hashxrcl  14322  hashgadd  14342  cjcl  15071  limsupcl  15439  limsuplt  15445  limsupval2  15446  limsupgre  15447  limsupbnd2  15449  cn1lem  15564  climcn1lem  15569  caucvgrlem2  15641  fsumrelem  15773  ackbijnn  15794  efcl  16048  sincl  16094  coscl  16095  rpnnen2lem9  16190  rpnnen2lem12  16193  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  sadaddlem  16436  sadasslem  16440  sadeq  16442  algcvg  16546  algcvgb  16548  algcvga  16549  algfx  16550  eucalgcvga  16556  eucalg  16557  xpsaddlem  17536  xpsvsca  17540  xpsle  17542  efgtf  19652  efgtlen  19656  efginvrel2  19657  efginvrel1  19658  efgsp1  19667  efgredleme  19673  efgredlemc  19675  efgred  19678  efgred2  19683  efgcpbllemb  19685  frgpnabllem1  19803  xpsdsval  24269  xrhmeo  24844  ioorcl  25478  volsup2  25506  volivth  25508  itg2const2  25642  itg2gt0  25661  dvcjbr  25853  dvcj  25854  dvfre  25855  rolle  25894  deg1xrcl  25987  plypf1  26117  resinf1o  26445  efif1olem4  26454  eff1olem  26457  logrncl  26476  relogcl  26484  asincl  26783  acoscl  26785  atancl  26791  asinrebnd  26811  dvatan  26845  leibpilem2  26851  leibpi  26852  areacl  26872  areage0  26873  divsqrtsumo1  26894  emcllem6  26911  emcllem7  26912  gamcl  26954  chtcl  27019  chpcl  27034  ppicl  27041  mucl  27051  sqff1o  27092  bposlem7  27201  dchrisum0lem2a  27428  mulog2sumlem1  27445  pntrsumo1  27476  pntrsumbnd  27477  pntrsumbnd2  27478  selbergr  27479  selberg3r  27480  selberg34r  27482  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2  27502  pntlemn  27511  pntlemj  27514  pntlemf  27516  pntlemo  27518  pntleml  27522  newf  27766  leftf  27777  rightf  27778  elmade  27779  ssltleft  27782  ssltright  27783  lnocoi  30686  nmlno0lem  30722  nmblolbii  30728  blocnilem  30733  blocni  30734  normcl  31054  occl  31233  hococli  31694  hosubcli  31698  hoaddcomi  31701  hodsi  31704  hoaddassi  31705  hocadddiri  31708  hocsubdiri  31709  ho2coi  31710  hoaddridi  31715  ho0coi  31717  hoid1ri  31719  honegsubi  31725  ho01i  31757  ho02i  31758  dmadjrn  31824  nmopnegi  31894  lnopaddi  31900  lnopsubi  31903  hoddii  31918  nmlnop0iALT  31924  lnopmi  31929  lnophsi  31930  lnopcoi  31932  lnopeq0lem1  31934  lnopeqi  31937  lnopunilem1  31939  lnopunilem2  31940  lnophmlem2  31946  nmbdoplbi  31953  nmcopexi  31956  nmcoplbi  31957  nmophmi  31960  lnopconi  31963  lnfn0i  31971  lnfnaddi  31972  lnfnmuli  31973  lnfnsubi  31975  nmbdfnlbi  31978  nmcfnexi  31980  nmcfnlbi  31981  lnfnconi  31984  riesz3i  31991  riesz4i  31992  cnlnadjlem2  31997  cnlnadjlem4  31999  cnlnadjlem6  32001  cnlnadjlem7  32002  nmopadjlem  32018  nmoptrii  32023  nmopcoi  32024  adjcoi  32029  nmopcoadji  32030  bracnln  32038  opsqrlem5  32073  opsqrlem6  32074  hmopidmchi  32080  hmopidmpji  32081  pjsdii  32084  pjddii  32085  pjcohocli  32132  mhmhmeotmd  33917  xrge0pluscn  33930  voliune  34219  volfiniune  34220  ddemeas  34226  eulerpartlems  34351  eulerpartlemsv3  34352  eulerpartlemgc  34353  eulerpartlemgvv  34367  eulerpartlemgf  34370  eulerpartlemgs2  34371  eulerpartlemn  34372  derangen  35159  subfacf  35162  subfacp1lem6  35172  subfaclim  35175  subfacval3  35176  msrrcl  35530  msrid  35532  circum  35661  fpwfvss  43401  liminfval2  45766  ismbl3  45984  ovolsplit  45986  stirlinglem13  46084  fourierdlem55  46159  fourierdlem77  46181  fourierdlem80  46184