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

Theorem ffvelrni 5702
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 5701 . 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 1701   -->wf 5288   ` cfv 5292
This theorem is referenced by:  f0cli  5709  cantnfval2  7415  cantnfle  7417  cantnflt  7418  cantnfres  7424  cantnfp1lem3  7427  cantnflem1b  7433  cantnflem1d  7435  cantnflem1  7436  wemapwe  7445  cnfcomlem  7447  cnfcom  7448  cnfcom3lem  7451  cnfcom3  7452  ackbij1lem14  7904  ackbij1lem15  7905  ackbij1lem16  7906  ackbij1lem18  7908  fpwwe2lem8  8304  nqercl  8600  uzssz  10294  axdc4uzlem  11091  hashkf  11386  hashcl  11397  hashxrcl  11398  hashgadd  11406  cjcl  11637  limsupcl  11994  limsuplt  12000  limsupval2  12001  limsupgre  12002  limsupbnd2  12004  cn1lem  12118  climcn1lem  12123  caucvgrlem2  12194  fsumrelem  12312  ackbijnn  12333  efcl  12411  sincl  12453  coscl  12454  rpnnen2lem9  12548  rpnnen2  12551  sadcaddlem  12695  sadadd2lem  12697  sadadd3  12699  sadaddlem  12704  sadasslem  12708  sadeq  12710  algcvg  12793  algcvgb  12795  algcvga  12796  algfx  12797  eucalgcvga  12803  eucalg  12804  xpsaddlem  13526  xpsvsca  13530  xpsle  13532  efgtf  15080  efgtlen  15084  efginvrel2  15085  efginvrel1  15086  efgsp1  15095  efgredleme  15101  efgredlemc  15103  efgred  15106  efgred2  15111  efgcpbllemb  15113  frgpnabllem1  15210  xpsdsval  17997  xrhmeo  18497  ioorcl  18985  volsup2  19013  volivth  19015  itg2const2  19149  itg2gt0  19168  dvcjbr  19351  dvcj  19352  dvfre  19353  rolle  19390  deg1xrcl  19521  plypf1  19647  resinf1o  19951  efif1olem4  19960  eff1olem  19963  logrncl  19978  relogcl  19985  asincl  20222  acoscl  20224  atancl  20230  asinrebnd  20250  dvatan  20284  leibpilem2  20290  leibpi  20291  areacl  20310  areage0  20311  divsqrsumo1  20331  emcllem6  20347  emcllem7  20348  chtcl  20400  chpcl  20415  ppicl  20422  mucl  20432  sqff1o  20473  bposlem7  20582  dchrisum0lem2a  20719  mulog2sumlem1  20736  pntrsumo1  20767  pntrsumbnd  20768  pntrsumbnd2  20769  selbergr  20770  selberg3r  20771  selberg34r  20773  pntrlog2bndlem1  20779  pntrlog2bndlem2  20780  pntrlog2bndlem3  20781  pntrlog2bndlem4  20782  pntrlog2bndlem5  20783  pntrlog2bndlem6  20785  pntrlog2bnd  20786  pntpbnd1a  20787  pntpbnd1  20788  pntpbnd2  20789  pntibndlem2  20793  pntlemn  20802  pntlemj  20805  pntlemf  20807  pntlemo  20809  pntleml  20813  lnocoi  21390  nmlno0lem  21426  nmblolbii  21432  blocnilem  21437  blocni  21438  normcl  21759  occl  21938  hococli  22400  hosubcli  22404  hoaddcomi  22407  hodsi  22410  hoaddassi  22411  hocadddiri  22414  hocsubdiri  22415  ho2coi  22416  hoaddid1i  22421  ho0coi  22423  hoid1ri  22425  honegsubi  22431  ho01i  22463  ho02i  22464  dmadjrn  22530  nmopnegi  22600  lnopaddi  22606  lnopsubi  22609  hoddii  22624  nmlnop0iALT  22630  lnopmi  22635  lnophsi  22636  lnopcoi  22638  lnopeq0lem1  22640  lnopeqi  22643  lnopunilem1  22645  lnopunilem2  22646  lnophmlem2  22652  nmbdoplbi  22659  nmcopexi  22662  nmcoplbi  22663  nmophmi  22666  lnopconi  22669  lnfn0i  22677  lnfnaddi  22678  lnfnmuli  22679  lnfnsubi  22681  nmbdfnlbi  22684  nmcfnexi  22686  nmcfnlbi  22687  lnfnconi  22690  riesz3i  22697  riesz4i  22698  cnlnadjlem2  22703  cnlnadjlem4  22705  cnlnadjlem6  22707  cnlnadjlem7  22708  nmopadjlem  22724  nmoptrii  22729  nmopcoi  22730  adjcoi  22735  nmopcoadji  22736  bracnln  22744  opsqrlem5  22779  opsqrlem6  22780  hmopidmchi  22786  hmopidmpji  22787  pjsdii  22790  pjddii  22791  pjcohocli  22838  mhmhmeotmd  23382  xrge0pluscn  23395  voliune  23759  volfiniune  23760  ballotlem7  23967  derangen  23987  subfacf  23990  subfacp1lem6  24000  subfaclim  24003  subfacval3  24004  vdegp1ai  24192  ghomgrpilem2  24277  circum  24291  dvcosre  26889  stirlinglem13  26983
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-fv 5300
  Copyright terms: Public domain W3C validator