Theorem ffvelrni 6969

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

Syntax hints:   → wi 4   ∈ wcel 2107  ⟶wf 6433  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445

This theorem is referenced by:  f0cli  6983  cantnfval2  9436  cantnfle  9438  cantnflt  9439  cantnfres  9444  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1d  9455  cantnflem1  9456  wemapwe  9464  cnfcomlem  9466  cnfcom  9467  cnfcom3lem  9470  cnfcom3  9471  ackbij1lem14  9998  ackbij1lem15  9999  ackbij1lem16  10000  ackbij1lem18  10002  fpwwe2lem7  10402  nqercl  10696  uzssz  12612  axdc4uzlem  13712  hashkf  14055  hashcl  14080  hashxrcl  14081  hashgadd  14101  cjcl  14825  limsupcl  15191  limsuplt  15197  limsupval2  15198  limsupgre  15199  limsupbnd2  15201  cn1lem  15316  climcn1lem  15321  caucvgrlem2  15395  fsumrelem  15528  ackbijnn  15549  efcl  15801  sincl  15844  coscl  15845  rpnnen2lem9  15940  rpnnen2lem12  15943  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  sadaddlem  16182  sadasslem  16186  sadeq  16188  algcvg  16290  algcvgb  16292  algcvga  16293  algfx  16294  eucalgcvga  16300  eucalg  16301  xpsaddlem  17293  xpsvsca  17297  xpsle  17299  efgtf  19337  efgtlen  19341  efginvrel2  19342  efginvrel1  19343  efgsp1  19352  efgredleme  19358  efgredlemc  19360  efgred  19363  efgred2  19368  efgcpbllemb  19370  frgpnabllem1  19483  xpsdsval  23543  xrhmeo  24118  ioorcl  24750  volsup2  24778  volivth  24780  itg2const2  24915  itg2gt0  24934  dvcjbr  25122  dvcj  25123  dvfre  25124  rolle  25163  deg1xrcl  25256  plypf1  25382  resinf1o  25701  efif1olem4  25710  eff1olem  25713  logrncl  25732  relogcl  25740  asincl  26032  acoscl  26034  atancl  26040  asinrebnd  26060  dvatan  26094  leibpilem2  26100  leibpi  26101  areacl  26121  areage0  26122  divsqrtsumo1  26142  emcllem6  26159  emcllem7  26160  gamcl  26202  chtcl  26267  chpcl  26282  ppicl  26289  mucl  26299  sqff1o  26340  bposlem7  26447  dchrisum0lem2a  26674  mulog2sumlem1  26691  pntrsumo1  26722  pntrsumbnd  26723  pntrsumbnd2  26724  selbergr  26725  selberg3r  26726  selberg34r  26728  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem2  26748  pntlemn  26757  pntlemj  26760  pntlemf  26762  pntlemo  26764  pntleml  26768  lnocoi  29128  nmlno0lem  29164  nmblolbii  29170  blocnilem  29175  blocni  29176  normcl  29496  occl  29675  hococli  30136  hosubcli  30140  hoaddcomi  30143  hodsi  30146  hoaddassi  30147  hocadddiri  30150  hocsubdiri  30151  ho2coi  30152  hoaddid1i  30157  ho0coi  30159  hoid1ri  30161  honegsubi  30167  ho01i  30199  ho02i  30200  dmadjrn  30266  nmopnegi  30336  lnopaddi  30342  lnopsubi  30345  hoddii  30360  nmlnop0iALT  30366  lnopmi  30371  lnophsi  30372  lnopcoi  30374  lnopeq0lem1  30376  lnopeqi  30379  lnopunilem1  30381  lnopunilem2  30382  lnophmlem2  30388  nmbdoplbi  30395  nmcopexi  30398  nmcoplbi  30399  nmophmi  30402  lnopconi  30405  lnfn0i  30413  lnfnaddi  30414  lnfnmuli  30415  lnfnsubi  30417  nmbdfnlbi  30420  nmcfnexi  30422  nmcfnlbi  30423  lnfnconi  30426  riesz3i  30433  riesz4i  30434  cnlnadjlem2  30439  cnlnadjlem4  30441  cnlnadjlem6  30443  cnlnadjlem7  30444  nmopadjlem  30460  nmoptrii  30465  nmopcoi  30466  adjcoi  30471  nmopcoadji  30472  bracnln  30480  opsqrlem5  30515  opsqrlem6  30516  hmopidmchi  30522  hmopidmpji  30523  pjsdii  30526  pjddii  30527  pjcohocli  30574  mhmhmeotmd  31886  xrge0pluscn  31899  voliune  32206  volfiniune  32207  ddemeas  32213  eulerpartlems  32336  eulerpartlemsv3  32337  eulerpartlemgc  32338  eulerpartlemgvv  32352  eulerpartlemgf  32355  eulerpartlemgs2  32356  eulerpartlemn  32357  derangen  33143  subfacf  33146  subfacp1lem6  33156  subfaclim  33159  subfacval3  33160  msrrcl  33514  msrid  33516  circum  33641  newf  34051  leftf  34058  rightf  34059  elmade  34060  ssltleft  34063  ssltright  34064  liminfval2  43316  ismbl3  43534  ovolsplit  43536  stirlinglem13  43634  fourierdlem55  43709  fourierdlem77  43731  fourierdlem80  43734