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

Theorem ffvelrn 5827
Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
Assertion
Ref Expression
ffvelrn  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )

Proof of Theorem ffvelrn
StepHypRef Expression
1 ffn 5550 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 5826 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 458 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5556 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3307 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 452 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
73, 6mpd 15 1  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   ran crn 4838    Fn wfn 5408   -->wf 5409   ` cfv 5413
This theorem is referenced by:  ffvelrni  5828  ffvelrnda  5829  dffo3  5843  foco2  5848  ffnfv  5853  ffvresb  5859  fcompt  5863  fsn2  5867  fvconst  5880  fcofo  5980  cocan1  5983  isocnv  6009  isocnv3  6011  isores2  6012  isopolem  6024  isosolem  6026  fovrn  6175  off  6279  fnwelem  6420  smofvon2  6577  smorndom  6589  omsmolem  6855  omsmo  6856  mapsncnv  7019  2dom  7138  xpdom2  7162  domunsncan  7167  xpmapenlem  7233  fiint  7342  ordiso2  7440  infdifsn  7567  cantnflem1  7601  wemapwe  7610  cnfcom3lem  7616  fseqenlem1  7861  finacn  7887  ackbij1lem12  8067  cofsmo  8105  cfsmolem  8106  cfcoflem  8108  coftr  8109  isf32lem6  8194  isf32lem7  8195  isf34lem7  8215  isf34lem6  8216  acncc  8276  axdc2lem  8284  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  ttukeylem6  8350  alephreg  8413  pwcfsdom  8414  canthp1lem2  8484  canthp1  8485  pwfseqlem1  8489  pwfseqlem4a  8492  gruf  8642  fsequb2  11270  axdc4uzlem  11276  seqf1o  11319  hashf1lem1  11659  eqs1  11716  shftf  11849  limsupgre  12230  rlimuni  12299  lo1resb  12313  o1resb  12315  o1of2  12361  o1rlimmul  12367  isercolllem1  12413  isercolllem2  12414  isercolllem3  12415  isercoll  12416  climsup  12418  iseralt  12433  sumeq2ii  12442  summolem2a  12464  isumcl  12500  isumshft  12574  climcndslem2  12585  climcnds  12586  mertenslem2  12617  rpnnen2lem10  12778  ruclem8  12791  ruclem12  12795  3dvds  12867  smueqlem  12957  nn0seqcvgd  13016  algrf  13019  eucalg  13033  phimullem  13123  pcmpt  13216  pcprod  13219  vdwlem11  13314  vdwnnlem3  13320  ramlb  13342  0ram  13343  ramcl  13352  imasaddfnlem  13708  imasaddflem  13710  mhmpropd  14699  ghmsub  14969  cntzmhm  15092  pj1ghm  15290  gsumzaddlem  15481  gsumzadd  15482  dprdfadd  15533  dprdf1o  15545  subgdmdprd  15547  gsumdixp  15670  lspcl  16007  psrbaglesupp  16388  psrbaglefi  16392  resspsrmul  16435  evlslem4  16519  fvcoe1  16560  psropprmul  16587  00ply1bas  16589  subrgvr1cl  16610  coe1mul2lem1  16615  coe1tmmul  16624  ply1coe  16639  znunit  16799  hauscmplem  17423  ptbasid  17560  ptpjcn  17596  upxp  17608  uptx  17610  txcmplem2  17627  xkopt  17640  txhmeo  17788  alexsubALTlem3  18033  nrginvrcn  18680  nmoi  18715  nmoleub  18718  cncfmet  18891  cnheibor  18933  evth  18937  pcopt  19000  pcopt2  19001  pcorevlem  19004  pi1xfrf  19031  pi1xfr  19033  pi1xfrcnvlem  19034  iscauf  19186  iscmet3lem1  19197  iscmet3lem2  19198  iscmet3  19199  causs  19204  bcthlem5  19234  bcth3  19237  ovolfcl  19316  ovolfioo  19317  ovolficc  19318  ovolficcss  19319  ovolfsval  19320  ovolmge0  19326  ovollb2lem  19337  ovolunlem1a  19345  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun  19354  ovolicc1  19365  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  voliunlem1  19397  volsup  19403  ioombl1lem2  19406  ovolfs2  19416  uniioovol  19424  uniiccvol  19425  uniioombllem3a  19429  uniioombllem3  19430  uniioombllem4  19431  uniioombllem5  19432  uniioombllem6  19433  dyadmbl  19445  volcn  19451  ismbf  19475  mbfadd  19506  mbfsub  19507  mbflimsup  19511  0plef  19517  itg1climres  19559  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfmul  19571  xrge0f  19576  itg2ge0  19580  itg2seq  19587  itg2uba  19588  itg2lea  19589  itg2eqa  19590  itg2splitlem  19593  itg2split  19594  itg2i1fseqle  19599  itg2i1fseq  19600  itg2i1fseq2  19601  itg2addlem  19603  bddmulibl  19683  ellimc3  19719  dvaddbr  19777  dvcobr  19785  dvcj  19789  dvfre  19790  dvcnvlem  19813  dvlip  19830  dvlipcn  19831  c1lip1  19834  evlslem3  19888  evl1val  19901  evl1sca  19903  pf1const  19919  tdeglem4  19936  tdeglem2  19937  coe1mul3  19975  ply1rem  20039  fta1g  20043  ig1pdvds  20052  plyf  20070  plyeq0lem  20082  plypf1  20084  plyaddlem  20087  plymullem  20088  plyco  20113  dgreq  20116  0dgrb  20118  coefv0  20119  coeaddlem  20120  coemullem  20121  coemulc  20126  plycn  20132  dgrcolem2  20145  plycjlem  20147  plycj  20148  plyrecj  20150  plyreres  20153  dvply1  20154  vieta1lem2  20181  vieta1  20182  elqaalem2  20190  aareccl  20196  aalioulem1  20202  ulmcaulem  20263  ulmcau  20264  ulmcn  20268  mtest  20273  psergf  20281  dvradcnv  20290  psercn2  20292  pserdvlem2  20297  pserdv2  20299  abelthlem6  20305  abelthlem8  20308  abelthlem9  20309  logtayl  20504  amgm  20782  ftalem1  20808  ftalem2  20809  ftalem3  20810  ftalem4  20811  ftalem5  20812  basellem2  20817  muinv  20931  dchrmulcl  20986  dchrinvcl  20990  dchrfi  20992  dchrghm  20993  dchrsum2  21005  dchrsum  21006  bposlem5  21025  lgscllem  21040  lgsval4a  21055  lgsneg  21056  lgsdir  21067  lgsdilem2  21068  lgsdi  21069  lgsne0  21070  lgseisenlem3  21088  rpvmasumlem  21134  dchrmusum2  21141  dchrvmasumiflem1  21148  dchrisum0ff  21154  dchrisum0flblem1  21155  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem2a  21164  usgrarnedg  21357  usgraedg4  21359  usgrares1  21377  usgrnloop  21516  cyclispthon  21573  fargshiftf  21576  usgrcyclnl2  21581  4cycl4dv  21607  vdgrnn0pnf  21633  ghgrplem2  21908  lnoadd  22212  lnosub  22213  nmosetre  22218  nmooge0  22221  nmoub3i  22227  nmounbi  22230  phoeqi  22312  ubthlem1  22325  h2hcau  22435  h2hlm  22436  hoscl  23201  homcl  23202  hodcl  23203  hoaddcl  23214  homulcl  23215  homulid2  23256  homco1  23257  homulass  23258  hoadddi  23259  hoadddir  23260  hoeq1  23286  hoeq2  23287  adjsym  23289  nmopsetretALT  23319  nmfnsetre  23333  cnvadj  23348  hhcno  23360  hhcnf  23361  nmopub2tALT  23365  nmopge0  23367  unopf1o  23372  unoplin  23376  counop  23377  nmfnleub2  23382  nmfnge0  23383  hmoplin  23398  eigvalcl  23417  lnop0  23422  hmops  23476  hmopm  23477  nlelchi  23517  leop2  23580  leopadd  23588  leopmuli  23589  leopnmid  23594  hmopidmchi  23607  pjinvari  23647  sticl  23671  fcomptf  24030  rge0scvg  24288  esumcst  24408  esumfzf  24412  esumfsup  24413  esumfsupre  24414  hasheuni  24428  measdivcstOLD  24531  derangsn  24809  subfacp1lem5  24823  subfacp1lem6  24824  pconcon  24871  sconpi1  24879  txsconlem  24880  cvxscon  24883  cvmliftphtlem  24957  cvmlift3lem2  24960  cvmlift3lem4  24962  cvmlift3lem6  24964  ghomgrpilem2  25050  ghomcl  25056  ghomgsg  25057  prodeq2ii  25192  prodmolem2a  25213  iprodcl  25267  faclim  25313  fprb  25343  soseq  25468  mblfinlem  26143  itg2addnclem  26155  upixp  26321  fdc  26339  seqpo  26341  incsequz  26342  incsequz2  26343  metf1o  26351  geomcau  26355  sstotbnd2  26373  prdsbnd  26392  ismtyima  26402  ismtyhmeolem  26403  heiborlem3  26412  heiborlem6  26415  heiborlem10  26419  bfplem1  26421  ghomco  26448  mzpclall  26674  mzprename  26696  rexrabdioph  26744  rmydioph  26975  rmxdioph  26977  expdiophlem2  26983  expdioph  26984  pw2f1ocnv  26998  kelac1  27029  uvcresum  27110  frlmsslsp  27116  frlmup1  27118  frlmup2  27119  lindfmm  27165  islindf4  27176  rngunsnply  27246  f1omvdconj  27257  ofsubid  27409  ofdivrec  27411  ofdivcan4  27412  ofdivdiv2  27413  dvconstbi  27419  refsum2cnlem1  27575  climinf  27599  stoweidlem26  27642  stoweidlem60  27676  stoweid  27679  2f1fvneq  27958  usgra2wlkspthlem2  28037  usgra2pthlem1  28040  el2wlkonotlem  28059  usg2wlkonot  28080  usg2wotspth  28081  frgrancvvdeqlemB  28141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
  Copyright terms: Public domain W3C validator