Theorem ffvelcdmi 7054

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

Syntax hints:   → wi 4   ∈ wcel 2106  ⟶wf 6512  ‘cfv 6516

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 2702  ax-sep 5276  ax-nul 5283  ax-pr 5404

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3419  df-v 3461  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-br 5126  df-opab 5188  df-id 5551  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-fv 6524

This theorem is referenced by:  f0cli  7068  cantnfval2  9629  cantnfle  9631  cantnflt  9632  cantnfres  9637  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1d  9648  cantnflem1  9649  wemapwe  9657  cnfcomlem  9659  cnfcom  9660  cnfcom3lem  9663  cnfcom3  9664  ackbij1lem14  10193  ackbij1lem15  10194  ackbij1lem16  10195  ackbij1lem18  10197  fpwwe2lem7  10597  nqercl  10891  uzssz  12808  axdc4uzlem  13913  hashkf  14257  hashcl  14281  hashxrcl  14282  hashgadd  14302  cjcl  15017  limsupcl  15382  limsuplt  15388  limsupval2  15389  limsupgre  15390  limsupbnd2  15392  cn1lem  15507  climcn1lem  15512  caucvgrlem2  15586  fsumrelem  15718  ackbijnn  15739  efcl  15991  sincl  16034  coscl  16035  rpnnen2lem9  16130  rpnnen2lem12  16133  sadcaddlem  16363  sadadd2lem  16365  sadadd3  16367  sadaddlem  16372  sadasslem  16376  sadeq  16378  algcvg  16478  algcvgb  16480  algcvga  16481  algfx  16482  eucalgcvga  16488  eucalg  16489  xpsaddlem  17484  xpsvsca  17488  xpsle  17490  efgtf  19533  efgtlen  19537  efginvrel2  19538  efginvrel1  19539  efgsp1  19548  efgredleme  19554  efgredlemc  19556  efgred  19559  efgred2  19564  efgcpbllemb  19566  frgpnabllem1  19680  xpsdsval  23786  xrhmeo  24361  ioorcl  24993  volsup2  25021  volivth  25023  itg2const2  25158  itg2gt0  25177  dvcjbr  25365  dvcj  25366  dvfre  25367  rolle  25406  deg1xrcl  25499  plypf1  25625  resinf1o  25944  efif1olem4  25953  eff1olem  25956  logrncl  25975  relogcl  25983  asincl  26275  acoscl  26277  atancl  26283  asinrebnd  26303  dvatan  26337  leibpilem2  26343  leibpi  26344  areacl  26364  areage0  26365  divsqrtsumo1  26385  emcllem6  26402  emcllem7  26403  gamcl  26445  chtcl  26510  chpcl  26525  ppicl  26532  mucl  26542  sqff1o  26583  bposlem7  26690  dchrisum0lem2a  26917  mulog2sumlem1  26934  pntrsumo1  26965  pntrsumbnd  26966  pntrsumbnd2  26967  selbergr  26968  selberg3r  26969  selberg34r  26971  pntrlog2bndlem1  26977  pntrlog2bndlem2  26978  pntrlog2bndlem3  26979  pntrlog2bndlem4  26980  pntrlog2bndlem5  26981  pntrlog2bndlem6  26983  pntrlog2bnd  26984  pntpbnd1a  26985  pntpbnd1  26986  pntpbnd2  26987  pntibndlem2  26991  pntlemn  27000  pntlemj  27003  pntlemf  27005  pntlemo  27007  pntleml  27011  newf  27246  leftf  27253  rightf  27254  elmade  27255  ssltleft  27258  ssltright  27259  lnocoi  29796  nmlno0lem  29832  nmblolbii  29838  blocnilem  29843  blocni  29844  normcl  30164  occl  30343  hococli  30804  hosubcli  30808  hoaddcomi  30811  hodsi  30814  hoaddassi  30815  hocadddiri  30818  hocsubdiri  30819  ho2coi  30820  hoaddridi  30825  ho0coi  30827  hoid1ri  30829  honegsubi  30835  ho01i  30867  ho02i  30868  dmadjrn  30934  nmopnegi  31004  lnopaddi  31010  lnopsubi  31013  hoddii  31028  nmlnop0iALT  31034  lnopmi  31039  lnophsi  31040  lnopcoi  31042  lnopeq0lem1  31044  lnopeqi  31047  lnopunilem1  31049  lnopunilem2  31050  lnophmlem2  31056  nmbdoplbi  31063  nmcopexi  31066  nmcoplbi  31067  nmophmi  31070  lnopconi  31073  lnfn0i  31081  lnfnaddi  31082  lnfnmuli  31083  lnfnsubi  31085  nmbdfnlbi  31088  nmcfnexi  31090  nmcfnlbi  31091  lnfnconi  31094  riesz3i  31101  riesz4i  31102  cnlnadjlem2  31107  cnlnadjlem4  31109  cnlnadjlem6  31111  cnlnadjlem7  31112  nmopadjlem  31128  nmoptrii  31133  nmopcoi  31134  adjcoi  31139  nmopcoadji  31140  bracnln  31148  opsqrlem5  31183  opsqrlem6  31184  hmopidmchi  31190  hmopidmpji  31191  pjsdii  31194  pjddii  31195  pjcohocli  31242  mhmhmeotmd  32631  xrge0pluscn  32644  voliune  32951  volfiniune  32952  ddemeas  32958  eulerpartlems  33083  eulerpartlemsv3  33084  eulerpartlemgc  33085  eulerpartlemgvv  33099  eulerpartlemgf  33102  eulerpartlemgs2  33103  eulerpartlemn  33104  derangen  33887  subfacf  33890  subfacp1lem6  33900  subfaclim  33903  subfacval3  33904  msrrcl  34258  msrid  34260  circum  34383  fpwfvss  41839  liminfval2  44162  ismbl3  44380  ovolsplit  44382  stirlinglem13  44480  fourierdlem55  44555  fourierdlem77  44577  fourierdlem80  44580