Theorem ffvelrni 6957

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

Syntax hints:   → wi 4   ∈ wcel 2110  ⟶wf 6428  ‘cfv 6432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-fv 6440

This theorem is referenced by:  f0cli  6971  cantnfval2  9405  cantnfle  9407  cantnflt  9408  cantnfres  9413  cantnfp1lem3  9416  cantnflem1b  9422  cantnflem1d  9424  cantnflem1  9425  wemapwe  9433  cnfcomlem  9435  cnfcom  9436  cnfcom3lem  9439  cnfcom3  9440  ackbij1lem14  9990  ackbij1lem15  9991  ackbij1lem16  9992  ackbij1lem18  9994  fpwwe2lem7  10394  nqercl  10688  uzssz  12602  axdc4uzlem  13701  hashkf  14044  hashcl  14069  hashxrcl  14070  hashgadd  14090  cjcl  14814  limsupcl  15180  limsuplt  15186  limsupval2  15187  limsupgre  15188  limsupbnd2  15190  cn1lem  15305  climcn1lem  15310  caucvgrlem2  15384  fsumrelem  15517  ackbijnn  15538  efcl  15790  sincl  15833  coscl  15834  rpnnen2lem9  15929  rpnnen2lem12  15932  sadcaddlem  16162  sadadd2lem  16164  sadadd3  16166  sadaddlem  16171  sadasslem  16175  sadeq  16177  algcvg  16279  algcvgb  16281  algcvga  16282  algfx  16283  eucalgcvga  16289  eucalg  16290  xpsaddlem  17282  xpsvsca  17286  xpsle  17288  efgtf  19326  efgtlen  19330  efginvrel2  19331  efginvrel1  19332  efgsp1  19341  efgredleme  19347  efgredlemc  19349  efgred  19352  efgred2  19357  efgcpbllemb  19359  frgpnabllem1  19472  xpsdsval  23532  xrhmeo  24107  ioorcl  24739  volsup2  24767  volivth  24769  itg2const2  24904  itg2gt0  24923  dvcjbr  25111  dvcj  25112  dvfre  25113  rolle  25152  deg1xrcl  25245  plypf1  25371  resinf1o  25690  efif1olem4  25699  eff1olem  25702  logrncl  25721  relogcl  25729  asincl  26021  acoscl  26023  atancl  26029  asinrebnd  26049  dvatan  26083  leibpilem2  26089  leibpi  26090  areacl  26110  areage0  26111  divsqrtsumo1  26131  emcllem6  26148  emcllem7  26149  gamcl  26191  chtcl  26256  chpcl  26271  ppicl  26278  mucl  26288  sqff1o  26329  bposlem7  26436  dchrisum0lem2a  26663  mulog2sumlem1  26680  pntrsumo1  26711  pntrsumbnd  26712  pntrsumbnd2  26713  selbergr  26714  selberg3r  26715  selberg34r  26717  pntrlog2bndlem1  26723  pntrlog2bndlem2  26724  pntrlog2bndlem3  26725  pntrlog2bndlem4  26726  pntrlog2bndlem5  26727  pntrlog2bndlem6  26729  pntrlog2bnd  26730  pntpbnd1a  26731  pntpbnd1  26732  pntpbnd2  26733  pntibndlem2  26737  pntlemn  26746  pntlemj  26749  pntlemf  26751  pntlemo  26753  pntleml  26757  lnocoi  29115  nmlno0lem  29151  nmblolbii  29157  blocnilem  29162  blocni  29163  normcl  29483  occl  29662  hococli  30123  hosubcli  30127  hoaddcomi  30130  hodsi  30133  hoaddassi  30134  hocadddiri  30137  hocsubdiri  30138  ho2coi  30139  hoaddid1i  30144  ho0coi  30146  hoid1ri  30148  honegsubi  30154  ho01i  30186  ho02i  30187  dmadjrn  30253  nmopnegi  30323  lnopaddi  30329  lnopsubi  30332  hoddii  30347  nmlnop0iALT  30353  lnopmi  30358  lnophsi  30359  lnopcoi  30361  lnopeq0lem1  30363  lnopeqi  30366  lnopunilem1  30368  lnopunilem2  30369  lnophmlem2  30375  nmbdoplbi  30382  nmcopexi  30385  nmcoplbi  30386  nmophmi  30389  lnopconi  30392  lnfn0i  30400  lnfnaddi  30401  lnfnmuli  30402  lnfnsubi  30404  nmbdfnlbi  30407  nmcfnexi  30409  nmcfnlbi  30410  lnfnconi  30413  riesz3i  30420  riesz4i  30421  cnlnadjlem2  30426  cnlnadjlem4  30428  cnlnadjlem6  30430  cnlnadjlem7  30431  nmopadjlem  30447  nmoptrii  30452  nmopcoi  30453  adjcoi  30458  nmopcoadji  30459  bracnln  30467  opsqrlem5  30502  opsqrlem6  30503  hmopidmchi  30509  hmopidmpji  30510  pjsdii  30513  pjddii  30514  pjcohocli  30561  mhmhmeotmd  31873  xrge0pluscn  31886  voliune  32193  volfiniune  32194  ddemeas  32200  eulerpartlems  32323  eulerpartlemsv3  32324  eulerpartlemgc  32325  eulerpartlemgvv  32339  eulerpartlemgf  32342  eulerpartlemgs2  32343  eulerpartlemn  32344  derangen  33130  subfacf  33133  subfacp1lem6  33143  subfaclim  33146  subfacval3  33147  msrrcl  33501  msrid  33503  circum  33628  newf  34038  leftf  34045  rightf  34046  elmade  34047  ssltleft  34050  ssltright  34051  liminfval2  43280  ismbl3  43498  ovolsplit  43500  stirlinglem13  43598  fourierdlem55  43673  fourierdlem77  43695  fourierdlem80  43698