Theorem ffvelcdmi 7037

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

Syntax hints:   → wi 4   ∈ wcel 2114  ⟶wf 6496  ‘cfv 6500

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 5243  ax-nul 5253  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508

This theorem is referenced by:  f0cli  7052  cantnfval2  9590  cantnfle  9592  cantnflt  9593  cantnfres  9598  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  wemapwe  9618  cnfcomlem  9620  cnfcom  9621  cnfcom3lem  9624  cnfcom3  9625  ackbij1lem14  10154  ackbij1lem15  10155  ackbij1lem16  10156  ackbij1lem18  10158  fpwwe2lem7  10560  nqercl  10854  uzssz  12784  axdc4uzlem  13918  hashkf  14267  hashcl  14291  hashxrcl  14292  hashgadd  14312  cjcl  15040  limsupcl  15408  limsuplt  15414  limsupval2  15415  limsupgre  15416  limsupbnd2  15418  cn1lem  15533  climcn1lem  15538  caucvgrlem2  15610  fsumrelem  15742  ackbijnn  15763  efcl  16017  sincl  16063  coscl  16064  rpnnen2lem9  16159  rpnnen2lem12  16162  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  sadaddlem  16405  sadasslem  16409  sadeq  16411  algcvg  16515  algcvgb  16517  algcvga  16518  algfx  16519  eucalgcvga  16525  eucalg  16526  xpsaddlem  17506  xpsvsca  17510  xpsle  17512  efgtf  19663  efgtlen  19667  efginvrel2  19668  efginvrel1  19669  efgsp1  19678  efgredleme  19684  efgredlemc  19686  efgred  19689  efgred2  19694  efgcpbllemb  19696  frgpnabllem1  19814  xpsdsval  24337  xrhmeo  24912  ioorcl  25546  volsup2  25574  volivth  25576  itg2const2  25710  itg2gt0  25729  dvcjbr  25921  dvcj  25922  dvfre  25923  rolle  25962  deg1xrcl  26055  plypf1  26185  resinf1o  26513  efif1olem4  26522  eff1olem  26525  logrncl  26544  relogcl  26552  asincl  26851  acoscl  26853  atancl  26859  asinrebnd  26879  dvatan  26913  leibpilem2  26919  leibpi  26920  areacl  26940  areage0  26941  divsqrtsumo1  26962  emcllem6  26979  emcllem7  26980  gamcl  27022  chtcl  27087  chpcl  27102  ppicl  27109  mucl  27119  sqff1o  27160  bposlem7  27269  dchrisum0lem2a  27496  mulog2sumlem1  27513  pntrsumo1  27544  pntrsumbnd  27545  pntrsumbnd2  27546  selbergr  27547  selberg3r  27548  selberg34r  27550  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem2  27570  pntlemn  27579  pntlemj  27582  pntlemf  27584  pntlemo  27586  pntleml  27590  newf  27846  leftf  27863  rightf  27864  elmade  27865  sltsleft  27868  sltsright  27869  lnocoi  30844  nmlno0lem  30880  nmblolbii  30886  blocnilem  30891  blocni  30892  normcl  31212  occl  31391  hococli  31852  hosubcli  31856  hoaddcomi  31859  hodsi  31862  hoaddassi  31863  hocadddiri  31866  hocsubdiri  31867  ho2coi  31868  hoaddridi  31873  ho0coi  31875  hoid1ri  31877  honegsubi  31883  ho01i  31915  ho02i  31916  dmadjrn  31982  nmopnegi  32052  lnopaddi  32058  lnopsubi  32061  hoddii  32076  nmlnop0iALT  32082  lnopmi  32087  lnophsi  32088  lnopcoi  32090  lnopeq0lem1  32092  lnopeqi  32095  lnopunilem1  32097  lnopunilem2  32098  lnophmlem2  32104  nmbdoplbi  32111  nmcopexi  32114  nmcoplbi  32115  nmophmi  32118  lnopconi  32121  lnfn0i  32129  lnfnaddi  32130  lnfnmuli  32131  lnfnsubi  32133  nmbdfnlbi  32136  nmcfnexi  32138  nmcfnlbi  32139  lnfnconi  32142  riesz3i  32149  riesz4i  32150  cnlnadjlem2  32155  cnlnadjlem4  32157  cnlnadjlem6  32159  cnlnadjlem7  32160  nmopadjlem  32176  nmoptrii  32181  nmopcoi  32182  adjcoi  32187  nmopcoadji  32188  bracnln  32196  opsqrlem5  32231  opsqrlem6  32232  hmopidmchi  32238  hmopidmpji  32239  pjsdii  32242  pjddii  32243  pjcohocli  32290  mhmhmeotmd  34104  xrge0pluscn  34117  voliune  34406  volfiniune  34407  ddemeas  34413  eulerpartlems  34537  eulerpartlemsv3  34538  eulerpartlemgc  34539  eulerpartlemgvv  34553  eulerpartlemgf  34556  eulerpartlemgs2  34557  eulerpartlemn  34558  derangen  35385  subfacf  35388  subfacp1lem6  35398  subfaclim  35401  subfacval3  35402  msrrcl  35756  msrid  35758  circum  35887  fpwfvss  43762  liminfval2  46120  ismbl3  46338  ovolsplit  46340  stirlinglem13  46438  fourierdlem55  46513  fourierdlem77  46535  fourierdlem80  46538