Theorem ffvelrni 6903

Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)

Hypothesis

Ref	Expression
ffvrni.1	⊢ 𝐹:𝐴⟶𝐵

Assertion

Ref	Expression
ffvelrni	⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelrni

Step	Hyp	Ref	Expression
1		ffvrni.1	. 2 ⊢ 𝐹:𝐴⟶𝐵
2		ffvelrn 6902	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
3	1, 2	mpan 690	1 ⊢ (𝐶 ∈ 𝐴 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2110  ⟶wf 6376  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-fv 6388

This theorem is referenced by:  f0cli  6917  cantnfval2  9284  cantnfle  9286  cantnflt  9287  cantnfres  9292  cantnfp1lem3  9295  cantnflem1b  9301  cantnflem1d  9303  cantnflem1  9304  wemapwe  9312  cnfcomlem  9314  cnfcom  9315  cnfcom3lem  9318  cnfcom3  9319  ackbij1lem14  9847  ackbij1lem15  9848  ackbij1lem16  9849  ackbij1lem18  9851  fpwwe2lem7  10251  nqercl  10545  uzssz  12459  axdc4uzlem  13556  hashkf  13898  hashcl  13923  hashxrcl  13924  hashgadd  13944  cjcl  14668  limsupcl  15034  limsuplt  15040  limsupval2  15041  limsupgre  15042  limsupbnd2  15044  cn1lem  15159  climcn1lem  15164  caucvgrlem2  15238  fsumrelem  15371  ackbijnn  15392  efcl  15644  sincl  15687  coscl  15688  rpnnen2lem9  15783  rpnnen2lem12  15786  sadcaddlem  16016  sadadd2lem  16018  sadadd3  16020  sadaddlem  16025  sadasslem  16029  sadeq  16031  algcvg  16133  algcvgb  16135  algcvga  16136  algfx  16137  eucalgcvga  16143  eucalg  16144  xpsaddlem  17078  xpsvsca  17082  xpsle  17084  efgtf  19112  efgtlen  19116  efginvrel2  19117  efginvrel1  19118  efgsp1  19127  efgredleme  19133  efgredlemc  19135  efgred  19138  efgred2  19143  efgcpbllemb  19145  frgpnabllem1  19258  xpsdsval  23279  xrhmeo  23843  ioorcl  24474  volsup2  24502  volivth  24504  itg2const2  24639  itg2gt0  24658  dvcjbr  24846  dvcj  24847  dvfre  24848  rolle  24887  deg1xrcl  24980  plypf1  25106  resinf1o  25425  efif1olem4  25434  eff1olem  25437  logrncl  25456  relogcl  25464  asincl  25756  acoscl  25758  atancl  25764  asinrebnd  25784  dvatan  25818  leibpilem2  25824  leibpi  25825  areacl  25845  areage0  25846  divsqrtsumo1  25866  emcllem6  25883  emcllem7  25884  gamcl  25926  chtcl  25991  chpcl  26006  ppicl  26013  mucl  26023  sqff1o  26064  bposlem7  26171  dchrisum0lem2a  26398  mulog2sumlem1  26415  pntrsumo1  26446  pntrsumbnd  26447  pntrsumbnd2  26448  selbergr  26449  selberg3r  26450  selberg34r  26452  pntrlog2bndlem1  26458  pntrlog2bndlem2  26459  pntrlog2bndlem3  26460  pntrlog2bndlem4  26461  pntrlog2bndlem5  26462  pntrlog2bndlem6  26464  pntrlog2bnd  26465  pntpbnd1a  26466  pntpbnd1  26467  pntpbnd2  26468  pntibndlem2  26472  pntlemn  26481  pntlemj  26484  pntlemf  26486  pntlemo  26488  pntleml  26492  lnocoi  28838  nmlno0lem  28874  nmblolbii  28880  blocnilem  28885  blocni  28886  normcl  29206  occl  29385  hococli  29846  hosubcli  29850  hoaddcomi  29853  hodsi  29856  hoaddassi  29857  hocadddiri  29860  hocsubdiri  29861  ho2coi  29862  hoaddid1i  29867  ho0coi  29869  hoid1ri  29871  honegsubi  29877  ho01i  29909  ho02i  29910  dmadjrn  29976  nmopnegi  30046  lnopaddi  30052  lnopsubi  30055  hoddii  30070  nmlnop0iALT  30076  lnopmi  30081  lnophsi  30082  lnopcoi  30084  lnopeq0lem1  30086  lnopeqi  30089  lnopunilem1  30091  lnopunilem2  30092  lnophmlem2  30098  nmbdoplbi  30105  nmcopexi  30108  nmcoplbi  30109  nmophmi  30112  lnopconi  30115  lnfn0i  30123  lnfnaddi  30124  lnfnmuli  30125  lnfnsubi  30127  nmbdfnlbi  30130  nmcfnexi  30132  nmcfnlbi  30133  lnfnconi  30136  riesz3i  30143  riesz4i  30144  cnlnadjlem2  30149  cnlnadjlem4  30151  cnlnadjlem6  30153  cnlnadjlem7  30154  nmopadjlem  30170  nmoptrii  30175  nmopcoi  30176  adjcoi  30181  nmopcoadji  30182  bracnln  30190  opsqrlem5  30225  opsqrlem6  30226  hmopidmchi  30232  hmopidmpji  30233  pjsdii  30236  pjddii  30237  pjcohocli  30284  mhmhmeotmd  31591  xrge0pluscn  31604  voliune  31909  volfiniune  31910  ddemeas  31916  eulerpartlems  32039  eulerpartlemsv3  32040  eulerpartlemgc  32041  eulerpartlemgvv  32055  eulerpartlemgf  32058  eulerpartlemgs2  32059  eulerpartlemn  32060  derangen  32847  subfacf  32850  subfacp1lem6  32860  subfaclim  32863  subfacval3  32864  msrrcl  33218  msrid  33220  circum  33345  newf  33779  leftf  33786  rightf  33787  elmade  33788  ssltleft  33791  ssltright  33792  liminfval2  42984  ismbl3  43202  ovolsplit  43204  stirlinglem13  43302  fourierdlem55  43377  fourierdlem77  43399  fourierdlem80  43402