Theorem ffvelrni 6942

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

Syntax hints:   → wi 4   ∈ wcel 2108  ⟶wf 6414  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426

This theorem is referenced by:  f0cli  6956  cantnfval2  9357  cantnfle  9359  cantnflt  9360  cantnfres  9365  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1d  9376  cantnflem1  9377  wemapwe  9385  cnfcomlem  9387  cnfcom  9388  cnfcom3lem  9391  cnfcom3  9392  ackbij1lem14  9920  ackbij1lem15  9921  ackbij1lem16  9922  ackbij1lem18  9924  fpwwe2lem7  10324  nqercl  10618  uzssz  12532  axdc4uzlem  13631  hashkf  13974  hashcl  13999  hashxrcl  14000  hashgadd  14020  cjcl  14744  limsupcl  15110  limsuplt  15116  limsupval2  15117  limsupgre  15118  limsupbnd2  15120  cn1lem  15235  climcn1lem  15240  caucvgrlem2  15314  fsumrelem  15447  ackbijnn  15468  efcl  15720  sincl  15763  coscl  15764  rpnnen2lem9  15859  rpnnen2lem12  15862  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadaddlem  16101  sadasslem  16105  sadeq  16107  algcvg  16209  algcvgb  16211  algcvga  16212  algfx  16213  eucalgcvga  16219  eucalg  16220  xpsaddlem  17201  xpsvsca  17205  xpsle  17207  efgtf  19243  efgtlen  19247  efginvrel2  19248  efginvrel1  19249  efgsp1  19258  efgredleme  19264  efgredlemc  19266  efgred  19269  efgred2  19274  efgcpbllemb  19276  frgpnabllem1  19389  xpsdsval  23442  xrhmeo  24015  ioorcl  24646  volsup2  24674  volivth  24676  itg2const2  24811  itg2gt0  24830  dvcjbr  25018  dvcj  25019  dvfre  25020  rolle  25059  deg1xrcl  25152  plypf1  25278  resinf1o  25597  efif1olem4  25606  eff1olem  25609  logrncl  25628  relogcl  25636  asincl  25928  acoscl  25930  atancl  25936  asinrebnd  25956  dvatan  25990  leibpilem2  25996  leibpi  25997  areacl  26017  areage0  26018  divsqrtsumo1  26038  emcllem6  26055  emcllem7  26056  gamcl  26098  chtcl  26163  chpcl  26178  ppicl  26185  mucl  26195  sqff1o  26236  bposlem7  26343  dchrisum0lem2a  26570  mulog2sumlem1  26587  pntrsumo1  26618  pntrsumbnd  26619  pntrsumbnd2  26620  selbergr  26621  selberg3r  26622  selberg34r  26624  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem2  26644  pntlemn  26653  pntlemj  26656  pntlemf  26658  pntlemo  26660  pntleml  26664  lnocoi  29020  nmlno0lem  29056  nmblolbii  29062  blocnilem  29067  blocni  29068  normcl  29388  occl  29567  hococli  30028  hosubcli  30032  hoaddcomi  30035  hodsi  30038  hoaddassi  30039  hocadddiri  30042  hocsubdiri  30043  ho2coi  30044  hoaddid1i  30049  ho0coi  30051  hoid1ri  30053  honegsubi  30059  ho01i  30091  ho02i  30092  dmadjrn  30158  nmopnegi  30228  lnopaddi  30234  lnopsubi  30237  hoddii  30252  nmlnop0iALT  30258  lnopmi  30263  lnophsi  30264  lnopcoi  30266  lnopeq0lem1  30268  lnopeqi  30271  lnopunilem1  30273  lnopunilem2  30274  lnophmlem2  30280  nmbdoplbi  30287  nmcopexi  30290  nmcoplbi  30291  nmophmi  30294  lnopconi  30297  lnfn0i  30305  lnfnaddi  30306  lnfnmuli  30307  lnfnsubi  30309  nmbdfnlbi  30312  nmcfnexi  30314  nmcfnlbi  30315  lnfnconi  30318  riesz3i  30325  riesz4i  30326  cnlnadjlem2  30331  cnlnadjlem4  30333  cnlnadjlem6  30335  cnlnadjlem7  30336  nmopadjlem  30352  nmoptrii  30357  nmopcoi  30358  adjcoi  30363  nmopcoadji  30364  bracnln  30372  opsqrlem5  30407  opsqrlem6  30408  hmopidmchi  30414  hmopidmpji  30415  pjsdii  30418  pjddii  30419  pjcohocli  30466  mhmhmeotmd  31779  xrge0pluscn  31792  voliune  32097  volfiniune  32098  ddemeas  32104  eulerpartlems  32227  eulerpartlemsv3  32228  eulerpartlemgc  32229  eulerpartlemgvv  32243  eulerpartlemgf  32246  eulerpartlemgs2  32247  eulerpartlemn  32248  derangen  33034  subfacf  33037  subfacp1lem6  33047  subfaclim  33050  subfacval3  33051  msrrcl  33405  msrid  33407  circum  33532  newf  33969  leftf  33976  rightf  33977  elmade  33978  ssltleft  33981  ssltright  33982  liminfval2  43199  ismbl3  43417  ovolsplit  43419  stirlinglem13  43517  fourierdlem55  43592  fourierdlem77  43614  fourierdlem80  43617