MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffvelrni Unicode version

Theorem ffvelrni 5664
Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)
Hypothesis
Ref Expression
ffvrni.1  |-  F : A
--> B
Assertion
Ref Expression
ffvelrni  |-  ( C  e.  A  ->  ( F `  C )  e.  B )

Proof of Theorem ffvelrni
StepHypRef Expression
1 ffvrni.1 . 2  |-  F : A
--> B
2 ffvelrn 5663 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2mpan 651 1  |-  ( C  e.  A  ->  ( F `  C )  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   -->wf 5251   ` cfv 5255
This theorem is referenced by:  f0cli  5671  cantnfval2  7370  cantnfle  7372  cantnflt  7373  cantnfres  7379  cantnfp1lem3  7382  cantnflem1b  7388  cantnflem1d  7390  cantnflem1  7391  wemapwe  7400  cnfcomlem  7402  cnfcom  7403  cnfcom3lem  7406  cnfcom3  7407  ackbij1lem14  7859  ackbij1lem15  7860  ackbij1lem16  7861  ackbij1lem18  7863  fpwwe2lem8  8259  nqercl  8555  uzssz  10247  axdc4uzlem  11044  hashkf  11339  hashcl  11350  hashxrcl  11351  hashgadd  11359  cjcl  11590  limsupcl  11947  limsuplt  11953  limsupval2  11954  limsupgre  11955  limsupbnd2  11957  cn1lem  12071  climcn1lem  12076  caucvgrlem2  12147  fsumrelem  12265  ackbijnn  12286  efcl  12364  sincl  12406  coscl  12407  rpnnen2lem9  12501  rpnnen2  12504  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadaddlem  12657  sadasslem  12661  sadeq  12663  algcvg  12746  algcvgb  12748  algcvga  12749  algfx  12750  eucalgcvga  12756  eucalg  12757  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  efgtf  15031  efgtlen  15035  efginvrel2  15036  efginvrel1  15037  efgsp1  15046  efgredleme  15052  efgredlemc  15054  efgred  15057  efgred2  15062  efgcpbllemb  15064  frgpnabllem1  15161  xpsdsval  17945  xrhmeo  18444  ioorcl  18932  volsup2  18960  volivth  18962  itg2const2  19096  itg2gt0  19115  dvcjbr  19298  dvcj  19299  dvfre  19300  rolle  19337  deg1xrcl  19468  plypf1  19594  resinf1o  19898  efif1olem4  19907  eff1olem  19910  logrncl  19925  relogcl  19932  asincl  20169  acoscl  20171  atancl  20177  asinrebnd  20197  dvatan  20231  leibpilem2  20237  leibpi  20238  areacl  20257  areage0  20258  divsqrsumo1  20278  emcllem6  20294  emcllem7  20295  chtcl  20347  chpcl  20362  ppicl  20369  mucl  20379  sqff1o  20420  bposlem7  20529  dchrisum0lem2a  20666  mulog2sumlem1  20683  pntrsumo1  20714  pntrsumbnd  20715  pntrsumbnd2  20716  selbergr  20717  selberg3r  20718  selberg34r  20720  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem2  20740  pntlemn  20749  pntlemj  20752  pntlemf  20754  pntlemo  20756  pntleml  20760  lnocoi  21335  nmlno0lem  21371  nmblolbii  21377  blocnilem  21382  blocni  21383  normcl  21704  occl  21883  hococli  22345  hosubcli  22349  hoaddcomi  22352  hodsi  22355  hoaddassi  22356  hocadddiri  22359  hocsubdiri  22360  ho2coi  22361  hoaddid1i  22366  ho0coi  22368  hoid1ri  22370  honegsubi  22376  ho01i  22408  ho02i  22409  dmadjrn  22475  nmopnegi  22545  lnopaddi  22551  lnopsubi  22554  hoddii  22569  nmlnop0iALT  22575  lnopmi  22580  lnophsi  22581  lnopcoi  22583  lnopeq0lem1  22585  lnopeqi  22588  lnopunilem1  22590  lnopunilem2  22591  lnophmlem2  22597  nmbdoplbi  22604  nmcopexi  22607  nmcoplbi  22608  nmophmi  22611  lnopconi  22614  lnfn0i  22622  lnfnaddi  22623  lnfnmuli  22624  lnfnsubi  22626  nmbdfnlbi  22629  nmcfnexi  22631  nmcfnlbi  22632  lnfnconi  22635  riesz3i  22642  riesz4i  22643  cnlnadjlem2  22648  cnlnadjlem4  22650  cnlnadjlem6  22652  cnlnadjlem7  22653  nmopadjlem  22669  nmoptrii  22674  nmopcoi  22675  adjcoi  22680  nmopcoadji  22681  bracnln  22689  opsqrlem5  22724  opsqrlem6  22725  hmopidmchi  22731  hmopidmpji  22732  pjsdii  22735  pjddii  22736  pjcohocli  22783  ballotlem7  23094  mhmhmeotmd  23300  xrge0pluscn  23322  derangen  23703  subfacf  23706  subfacp1lem6  23716  subfaclim  23719  subfacval3  23720  vdegp1ai  23908  ghomgrpilem2  23993  circum  24007  seqzp2  25355  dvcosre  27741  stirlinglem13  27835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263
  Copyright terms: Public domain W3C validator