Theorem ffvelcdmi 7102

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

Syntax hints:   → wi 4   ∈ wcel 2105  ⟶wf 6558  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570

This theorem is referenced by:  f0cli  7117  cantnfval2  9706  cantnfle  9708  cantnflt  9709  cantnfres  9714  cantnfp1lem3  9717  cantnflem1b  9723  cantnflem1d  9725  cantnflem1  9726  wemapwe  9734  cnfcomlem  9736  cnfcom  9737  cnfcom3lem  9740  cnfcom3  9741  ackbij1lem14  10269  ackbij1lem15  10270  ackbij1lem16  10271  ackbij1lem18  10273  fpwwe2lem7  10674  nqercl  10968  uzssz  12896  axdc4uzlem  14020  hashkf  14367  hashcl  14391  hashxrcl  14392  hashgadd  14412  cjcl  15140  limsupcl  15505  limsuplt  15511  limsupval2  15512  limsupgre  15513  limsupbnd2  15515  cn1lem  15630  climcn1lem  15635  caucvgrlem2  15707  fsumrelem  15839  ackbijnn  15860  efcl  16114  sincl  16158  coscl  16159  rpnnen2lem9  16254  rpnnen2lem12  16257  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadaddlem  16499  sadasslem  16503  sadeq  16505  algcvg  16609  algcvgb  16611  algcvga  16612  algfx  16613  eucalgcvga  16619  eucalg  16620  xpsaddlem  17619  xpsvsca  17623  xpsle  17625  efgtf  19754  efgtlen  19758  efginvrel2  19759  efginvrel1  19760  efgsp1  19769  efgredleme  19775  efgredlemc  19777  efgred  19780  efgred2  19785  efgcpbllemb  19787  frgpnabllem1  19905  xpsdsval  24406  xrhmeo  24990  ioorcl  25625  volsup2  25653  volivth  25655  itg2const2  25790  itg2gt0  25809  dvcjbr  26001  dvcj  26002  dvfre  26003  rolle  26042  deg1xrcl  26135  plypf1  26265  resinf1o  26592  efif1olem4  26601  eff1olem  26604  logrncl  26623  relogcl  26631  asincl  26930  acoscl  26932  atancl  26938  asinrebnd  26958  dvatan  26992  leibpilem2  26998  leibpi  26999  areacl  27019  areage0  27020  divsqrtsumo1  27041  emcllem6  27058  emcllem7  27059  gamcl  27101  chtcl  27166  chpcl  27181  ppicl  27188  mucl  27198  sqff1o  27239  bposlem7  27348  dchrisum0lem2a  27575  mulog2sumlem1  27592  pntrsumo1  27623  pntrsumbnd  27624  pntrsumbnd2  27625  selbergr  27626  selberg3r  27627  selberg34r  27629  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2  27649  pntlemn  27658  pntlemj  27661  pntlemf  27663  pntlemo  27665  pntleml  27669  newf  27911  leftf  27918  rightf  27919  elmade  27920  ssltleft  27923  ssltright  27924  lnocoi  30785  nmlno0lem  30821  nmblolbii  30827  blocnilem  30832  blocni  30833  normcl  31153  occl  31332  hococli  31793  hosubcli  31797  hoaddcomi  31800  hodsi  31803  hoaddassi  31804  hocadddiri  31807  hocsubdiri  31808  ho2coi  31809  hoaddridi  31814  ho0coi  31816  hoid1ri  31818  honegsubi  31824  ho01i  31856  ho02i  31857  dmadjrn  31923  nmopnegi  31993  lnopaddi  31999  lnopsubi  32002  hoddii  32017  nmlnop0iALT  32023  lnopmi  32028  lnophsi  32029  lnopcoi  32031  lnopeq0lem1  32033  lnopeqi  32036  lnopunilem1  32038  lnopunilem2  32039  lnophmlem2  32045  nmbdoplbi  32052  nmcopexi  32055  nmcoplbi  32056  nmophmi  32059  lnopconi  32062  lnfn0i  32070  lnfnaddi  32071  lnfnmuli  32072  lnfnsubi  32074  nmbdfnlbi  32077  nmcfnexi  32079  nmcfnlbi  32080  lnfnconi  32083  riesz3i  32090  riesz4i  32091  cnlnadjlem2  32096  cnlnadjlem4  32098  cnlnadjlem6  32100  cnlnadjlem7  32101  nmopadjlem  32117  nmoptrii  32122  nmopcoi  32123  adjcoi  32128  nmopcoadji  32129  bracnln  32137  opsqrlem5  32172  opsqrlem6  32173  hmopidmchi  32179  hmopidmpji  32180  pjsdii  32183  pjddii  32184  pjcohocli  32231  mhmhmeotmd  33887  xrge0pluscn  33900  voliune  34209  volfiniune  34210  ddemeas  34216  eulerpartlems  34341  eulerpartlemsv3  34342  eulerpartlemgc  34343  eulerpartlemgvv  34357  eulerpartlemgf  34360  eulerpartlemgs2  34361  eulerpartlemn  34362  derangen  35156  subfacf  35159  subfacp1lem6  35169  subfaclim  35172  subfacval3  35173  msrrcl  35527  msrid  35529  circum  35658  fpwfvss  43401  liminfval2  45723  ismbl3  45941  ovolsplit  45943  stirlinglem13  46041  fourierdlem55  46116  fourierdlem77  46138  fourierdlem80  46141