Theorem ffvelcdmi 7072

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

Syntax hints:   → wi 4   ∈ wcel 2108  ⟶wf 6526  ‘cfv 6530

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538

This theorem is referenced by:  f0cli  7087  cantnfval2  9681  cantnfle  9683  cantnflt  9684  cantnfres  9689  cantnfp1lem3  9692  cantnflem1b  9698  cantnflem1d  9700  cantnflem1  9701  wemapwe  9709  cnfcomlem  9711  cnfcom  9712  cnfcom3lem  9715  cnfcom3  9716  ackbij1lem14  10244  ackbij1lem15  10245  ackbij1lem16  10246  ackbij1lem18  10248  fpwwe2lem7  10649  nqercl  10943  uzssz  12871  axdc4uzlem  13999  hashkf  14348  hashcl  14372  hashxrcl  14373  hashgadd  14393  cjcl  15122  limsupcl  15487  limsuplt  15493  limsupval2  15494  limsupgre  15495  limsupbnd2  15497  cn1lem  15612  climcn1lem  15617  caucvgrlem2  15689  fsumrelem  15821  ackbijnn  15842  efcl  16096  sincl  16142  coscl  16143  rpnnen2lem9  16238  rpnnen2lem12  16241  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  sadaddlem  16483  sadasslem  16487  sadeq  16489  algcvg  16593  algcvgb  16595  algcvga  16596  algfx  16597  eucalgcvga  16603  eucalg  16604  xpsaddlem  17585  xpsvsca  17589  xpsle  17591  efgtf  19701  efgtlen  19705  efginvrel2  19706  efginvrel1  19707  efgsp1  19716  efgredleme  19722  efgredlemc  19724  efgred  19727  efgred2  19732  efgcpbllemb  19734  frgpnabllem1  19852  xpsdsval  24318  xrhmeo  24893  ioorcl  25528  volsup2  25556  volivth  25558  itg2const2  25692  itg2gt0  25711  dvcjbr  25903  dvcj  25904  dvfre  25905  rolle  25944  deg1xrcl  26037  plypf1  26167  resinf1o  26495  efif1olem4  26504  eff1olem  26507  logrncl  26526  relogcl  26534  asincl  26833  acoscl  26835  atancl  26841  asinrebnd  26861  dvatan  26895  leibpilem2  26901  leibpi  26902  areacl  26922  areage0  26923  divsqrtsumo1  26944  emcllem6  26961  emcllem7  26962  gamcl  27004  chtcl  27069  chpcl  27084  ppicl  27091  mucl  27101  sqff1o  27142  bposlem7  27251  dchrisum0lem2a  27478  mulog2sumlem1  27495  pntrsumo1  27526  pntrsumbnd  27527  pntrsumbnd2  27528  selbergr  27529  selberg3r  27530  selberg34r  27532  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem4  27541  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntibndlem2  27552  pntlemn  27561  pntlemj  27564  pntlemf  27566  pntlemo  27568  pntleml  27572  newf  27814  leftf  27821  rightf  27822  elmade  27823  ssltleft  27826  ssltright  27827  lnocoi  30684  nmlno0lem  30720  nmblolbii  30726  blocnilem  30731  blocni  30732  normcl  31052  occl  31231  hococli  31692  hosubcli  31696  hoaddcomi  31699  hodsi  31702  hoaddassi  31703  hocadddiri  31706  hocsubdiri  31707  ho2coi  31708  hoaddridi  31713  ho0coi  31715  hoid1ri  31717  honegsubi  31723  ho01i  31755  ho02i  31756  dmadjrn  31822  nmopnegi  31892  lnopaddi  31898  lnopsubi  31901  hoddii  31916  nmlnop0iALT  31922  lnopmi  31927  lnophsi  31928  lnopcoi  31930  lnopeq0lem1  31932  lnopeqi  31935  lnopunilem1  31937  lnopunilem2  31938  lnophmlem2  31944  nmbdoplbi  31951  nmcopexi  31954  nmcoplbi  31955  nmophmi  31958  lnopconi  31961  lnfn0i  31969  lnfnaddi  31970  lnfnmuli  31971  lnfnsubi  31973  nmbdfnlbi  31976  nmcfnexi  31978  nmcfnlbi  31979  lnfnconi  31982  riesz3i  31989  riesz4i  31990  cnlnadjlem2  31995  cnlnadjlem4  31997  cnlnadjlem6  31999  cnlnadjlem7  32000  nmopadjlem  32016  nmoptrii  32021  nmopcoi  32022  adjcoi  32027  nmopcoadji  32028  bracnln  32036  opsqrlem5  32071  opsqrlem6  32072  hmopidmchi  32078  hmopidmpji  32079  pjsdii  32082  pjddii  32083  pjcohocli  32130  mhmhmeotmd  33904  xrge0pluscn  33917  voliune  34206  volfiniune  34207  ddemeas  34213  eulerpartlems  34338  eulerpartlemsv3  34339  eulerpartlemgc  34340  eulerpartlemgvv  34354  eulerpartlemgf  34357  eulerpartlemgs2  34358  eulerpartlemn  34359  derangen  35140  subfacf  35143  subfacp1lem6  35153  subfaclim  35156  subfacval3  35157  msrrcl  35511  msrid  35513  circum  35642  fpwfvss  43383  liminfval2  45745  ismbl3  45963  ovolsplit  45965  stirlinglem13  46063  fourierdlem55  46138  fourierdlem77  46160  fourierdlem80  46163