Theorem ffvelcdmi 7103

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

Syntax hints:   → wi 4   ∈ wcel 2108  ⟶wf 6557  ‘cfv 6561

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is referenced by:  f0cli  7118  cantnfval2  9709  cantnfle  9711  cantnflt  9712  cantnfres  9717  cantnfp1lem3  9720  cantnflem1b  9726  cantnflem1d  9728  cantnflem1  9729  wemapwe  9737  cnfcomlem  9739  cnfcom  9740  cnfcom3lem  9743  cnfcom3  9744  ackbij1lem14  10272  ackbij1lem15  10273  ackbij1lem16  10274  ackbij1lem18  10276  fpwwe2lem7  10677  nqercl  10971  uzssz  12899  axdc4uzlem  14024  hashkf  14371  hashcl  14395  hashxrcl  14396  hashgadd  14416  cjcl  15144  limsupcl  15509  limsuplt  15515  limsupval2  15516  limsupgre  15517  limsupbnd2  15519  cn1lem  15634  climcn1lem  15639  caucvgrlem2  15711  fsumrelem  15843  ackbijnn  15864  efcl  16118  sincl  16162  coscl  16163  rpnnen2lem9  16258  rpnnen2lem12  16261  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadaddlem  16503  sadasslem  16507  sadeq  16509  algcvg  16613  algcvgb  16615  algcvga  16616  algfx  16617  eucalgcvga  16623  eucalg  16624  xpsaddlem  17618  xpsvsca  17622  xpsle  17624  efgtf  19740  efgtlen  19744  efginvrel2  19745  efginvrel1  19746  efgsp1  19755  efgredleme  19761  efgredlemc  19763  efgred  19766  efgred2  19771  efgcpbllemb  19773  frgpnabllem1  19891  xpsdsval  24391  xrhmeo  24977  ioorcl  25612  volsup2  25640  volivth  25642  itg2const2  25776  itg2gt0  25795  dvcjbr  25987  dvcj  25988  dvfre  25989  rolle  26028  deg1xrcl  26121  plypf1  26251  resinf1o  26578  efif1olem4  26587  eff1olem  26590  logrncl  26609  relogcl  26617  asincl  26916  acoscl  26918  atancl  26924  asinrebnd  26944  dvatan  26978  leibpilem2  26984  leibpi  26985  areacl  27005  areage0  27006  divsqrtsumo1  27027  emcllem6  27044  emcllem7  27045  gamcl  27087  chtcl  27152  chpcl  27167  ppicl  27174  mucl  27184  sqff1o  27225  bposlem7  27334  dchrisum0lem2a  27561  mulog2sumlem1  27578  pntrsumo1  27609  pntrsumbnd  27610  pntrsumbnd2  27611  selbergr  27612  selberg3r  27613  selberg34r  27615  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntpbnd2  27631  pntibndlem2  27635  pntlemn  27644  pntlemj  27647  pntlemf  27649  pntlemo  27651  pntleml  27655  newf  27897  leftf  27904  rightf  27905  elmade  27906  ssltleft  27909  ssltright  27910  lnocoi  30776  nmlno0lem  30812  nmblolbii  30818  blocnilem  30823  blocni  30824  normcl  31144  occl  31323  hococli  31784  hosubcli  31788  hoaddcomi  31791  hodsi  31794  hoaddassi  31795  hocadddiri  31798  hocsubdiri  31799  ho2coi  31800  hoaddridi  31805  ho0coi  31807  hoid1ri  31809  honegsubi  31815  ho01i  31847  ho02i  31848  dmadjrn  31914  nmopnegi  31984  lnopaddi  31990  lnopsubi  31993  hoddii  32008  nmlnop0iALT  32014  lnopmi  32019  lnophsi  32020  lnopcoi  32022  lnopeq0lem1  32024  lnopeqi  32027  lnopunilem1  32029  lnopunilem2  32030  lnophmlem2  32036  nmbdoplbi  32043  nmcopexi  32046  nmcoplbi  32047  nmophmi  32050  lnopconi  32053  lnfn0i  32061  lnfnaddi  32062  lnfnmuli  32063  lnfnsubi  32065  nmbdfnlbi  32068  nmcfnexi  32070  nmcfnlbi  32071  lnfnconi  32074  riesz3i  32081  riesz4i  32082  cnlnadjlem2  32087  cnlnadjlem4  32089  cnlnadjlem6  32091  cnlnadjlem7  32092  nmopadjlem  32108  nmoptrii  32113  nmopcoi  32114  adjcoi  32119  nmopcoadji  32120  bracnln  32128  opsqrlem5  32163  opsqrlem6  32164  hmopidmchi  32170  hmopidmpji  32171  pjsdii  32174  pjddii  32175  pjcohocli  32222  mhmhmeotmd  33926  xrge0pluscn  33939  voliune  34230  volfiniune  34231  ddemeas  34237  eulerpartlems  34362  eulerpartlemsv3  34363  eulerpartlemgc  34364  eulerpartlemgvv  34378  eulerpartlemgf  34381  eulerpartlemgs2  34382  eulerpartlemn  34383  derangen  35177  subfacf  35180  subfacp1lem6  35190  subfaclim  35193  subfacval3  35194  msrrcl  35548  msrid  35550  circum  35679  fpwfvss  43425  liminfval2  45783  ismbl3  46001  ovolsplit  46003  stirlinglem13  46101  fourierdlem55  46176  fourierdlem77  46198  fourierdlem80  46201