Theorem ffvelcdmi 7085

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

Syntax hints:   → wi 4   ∈ wcel 2106  ⟶wf 6539  ‘cfv 6543

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is referenced by:  f0cli  7099  cantnfval2  9666  cantnfle  9668  cantnflt  9669  cantnfres  9674  cantnfp1lem3  9677  cantnflem1b  9683  cantnflem1d  9685  cantnflem1  9686  wemapwe  9694  cnfcomlem  9696  cnfcom  9697  cnfcom3lem  9700  cnfcom3  9701  ackbij1lem14  10230  ackbij1lem15  10231  ackbij1lem16  10232  ackbij1lem18  10234  fpwwe2lem7  10634  nqercl  10928  uzssz  12845  axdc4uzlem  13950  hashkf  14294  hashcl  14318  hashxrcl  14319  hashgadd  14339  cjcl  15054  limsupcl  15419  limsuplt  15425  limsupval2  15426  limsupgre  15427  limsupbnd2  15429  cn1lem  15544  climcn1lem  15549  caucvgrlem2  15623  fsumrelem  15755  ackbijnn  15776  efcl  16028  sincl  16071  coscl  16072  rpnnen2lem9  16167  rpnnen2lem12  16170  sadcaddlem  16400  sadadd2lem  16402  sadadd3  16404  sadaddlem  16409  sadasslem  16413  sadeq  16415  algcvg  16515  algcvgb  16517  algcvga  16518  algfx  16519  eucalgcvga  16525  eucalg  16526  xpsaddlem  17521  xpsvsca  17525  xpsle  17527  efgtf  19592  efgtlen  19596  efginvrel2  19597  efginvrel1  19598  efgsp1  19607  efgredleme  19613  efgredlemc  19615  efgred  19618  efgred2  19623  efgcpbllemb  19625  frgpnabllem1  19743  xpsdsval  23894  xrhmeo  24469  ioorcl  25101  volsup2  25129  volivth  25131  itg2const2  25266  itg2gt0  25285  dvcjbr  25473  dvcj  25474  dvfre  25475  rolle  25514  deg1xrcl  25607  plypf1  25733  resinf1o  26052  efif1olem4  26061  eff1olem  26064  logrncl  26083  relogcl  26091  asincl  26385  acoscl  26387  atancl  26393  asinrebnd  26413  dvatan  26447  leibpilem2  26453  leibpi  26454  areacl  26474  areage0  26475  divsqrtsumo1  26495  emcllem6  26512  emcllem7  26513  gamcl  26555  chtcl  26620  chpcl  26635  ppicl  26642  mucl  26652  sqff1o  26693  bposlem7  26800  dchrisum0lem2a  27027  mulog2sumlem1  27044  pntrsumo1  27075  pntrsumbnd  27076  pntrsumbnd2  27077  selbergr  27078  selberg3r  27079  selberg34r  27081  pntrlog2bndlem1  27087  pntrlog2bndlem2  27088  pntrlog2bndlem3  27089  pntrlog2bndlem4  27090  pntrlog2bndlem5  27091  pntrlog2bndlem6  27093  pntrlog2bnd  27094  pntpbnd1a  27095  pntpbnd1  27096  pntpbnd2  27097  pntibndlem2  27101  pntlemn  27110  pntlemj  27113  pntlemf  27115  pntlemo  27117  pntleml  27121  newf  27361  leftf  27368  rightf  27369  elmade  27370  ssltleft  27373  ssltright  27374  lnocoi  30048  nmlno0lem  30084  nmblolbii  30090  blocnilem  30095  blocni  30096  normcl  30416  occl  30595  hococli  31056  hosubcli  31060  hoaddcomi  31063  hodsi  31066  hoaddassi  31067  hocadddiri  31070  hocsubdiri  31071  ho2coi  31072  hoaddridi  31077  ho0coi  31079  hoid1ri  31081  honegsubi  31087  ho01i  31119  ho02i  31120  dmadjrn  31186  nmopnegi  31256  lnopaddi  31262  lnopsubi  31265  hoddii  31280  nmlnop0iALT  31286  lnopmi  31291  lnophsi  31292  lnopcoi  31294  lnopeq0lem1  31296  lnopeqi  31299  lnopunilem1  31301  lnopunilem2  31302  lnophmlem2  31308  nmbdoplbi  31315  nmcopexi  31318  nmcoplbi  31319  nmophmi  31322  lnopconi  31325  lnfn0i  31333  lnfnaddi  31334  lnfnmuli  31335  lnfnsubi  31337  nmbdfnlbi  31340  nmcfnexi  31342  nmcfnlbi  31343  lnfnconi  31346  riesz3i  31353  riesz4i  31354  cnlnadjlem2  31359  cnlnadjlem4  31361  cnlnadjlem6  31363  cnlnadjlem7  31364  nmopadjlem  31380  nmoptrii  31385  nmopcoi  31386  adjcoi  31391  nmopcoadji  31392  bracnln  31400  opsqrlem5  31435  opsqrlem6  31436  hmopidmchi  31442  hmopidmpji  31443  pjsdii  31446  pjddii  31447  pjcohocli  31494  mhmhmeotmd  32976  xrge0pluscn  32989  voliune  33296  volfiniune  33297  ddemeas  33303  eulerpartlems  33428  eulerpartlemsv3  33429  eulerpartlemgc  33430  eulerpartlemgvv  33444  eulerpartlemgf  33447  eulerpartlemgs2  33448  eulerpartlemn  33449  derangen  34232  subfacf  34235  subfacp1lem6  34245  subfaclim  34248  subfacval3  34249  msrrcl  34603  msrid  34605  circum  34728  fpwfvss  42245  liminfval2  44563  ismbl3  44781  ovolsplit  44783  stirlinglem13  44881  fourierdlem55  44956  fourierdlem77  44978  fourierdlem80  44981