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

Theorem ffvelrn 5836
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 5554 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 5835 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 471 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5560 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3350 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 465 . 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 setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   ran crn 4836    Fn wfn 5408   -->wf 5409   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  ffvelrni  5837  ffvelrnda  5838  dffo3  5853  foco2  5858  ffnfv  5864  ffvresb  5869  fcompt  5874  fsn2  5878  fvconst  5892  fcofo  5987  cocan1  5990  isocnv  6016  isocnv3  6018  isores2  6019  isopolem  6031  isosolem  6033  fovrn  6228  off  6329  fnwelem  6682  smofvon2  6809  smorndom  6821  omsmolem  7084  omsmo  7085  mapsncnv  7251  2dom  7374  xpdom2  7398  domunsncan  7403  xpmapenlem  7470  fiint  7580  ordiso2  7721  infdifsn  7854  cantnflem1  7889  cantnflem1OLD  7912  wemapwe  7920  wemapweOLD  7921  cnfcom3lem  7928  cnfcom3lemOLD  7936  fseqenlem1  8186  finacn  8212  ackbij1lem12  8392  cofsmo  8430  cfsmolem  8431  cfcoflem  8433  coftr  8434  isf32lem6  8519  isf32lem7  8520  isf34lem7  8540  isf34lem6  8541  acncc  8601  axdc2lem  8609  axdc3lem2  8612  axdc3lem4  8614  axdc4lem  8616  axcclem  8618  ttukeylem6  8675  alephreg  8738  pwcfsdom  8739  canthp1lem2  8812  canthp1  8813  pwfseqlem1  8817  pwfseqlem4a  8820  gruf  8970  fsequb2  11790  axdc4uzlem  11796  seqf1o  11839  hashf1lem1  12200  eqs1  12292  shftf  12560  limsupgre  12951  rlimuni  13020  lo1resb  13034  o1resb  13036  o1of2  13082  o1rlimmul  13088  isercolllem1  13134  isercolllem2  13135  isercolllem3  13136  isercoll  13137  climsup  13139  iseralt  13154  sumeq2ii  13162  summolem2a  13184  isumcl  13220  isumshft  13294  climcndslem2  13305  climcnds  13306  mertenslem2  13337  rpnnen2lem10  13498  ruclem8  13511  ruclem12  13515  3dvds  13588  smueqlem  13678  nn0seqcvgd  13737  algrf  13740  eucalg  13754  phimullem  13846  pcmpt  13946  pcprod  13949  vdwlem11  14044  vdwnnlem3  14050  ramlb  14072  0ram  14073  ramcl  14082  imasaddfnlem  14458  imasaddflem  14460  mhmpropd  15462  ghmsub  15746  cntzmhm  15847  f1omvdconj  15943  pj1ghm  16191  gsumzaddlem  16399  gsumzadd  16400  gsumzaddlemOLD  16401  gsumzaddOLD  16402  dprdfadd  16500  dprdfaddOLD  16507  dprdf1o  16519  subgdmdprd  16521  gsumdixpOLD  16690  gsumdixp  16691  lspcl  17037  psrbaglesupp  17415  psrbaglesuppOLD  17416  psrbaglefi  17421  psrbaglefiOLD  17422  resspsrmul  17469  evlslem4OLD  17570  evlslem4  17571  evlslem3  17580  fvcoe1  17643  psropprmul  17673  00ply1bas  17675  subrgvr1cl  17696  coe1mul2lem1  17701  coe1tmmul  17710  ply1coe  17726  ply1coeOLD  17727  evl1val  17743  evl1sca  17748  pf1const  17760  znunit  17976  frlmsslsp  18203  frlmsslspOLD  18204  frlmup2  18207  lindfmm  18236  islindf4  18247  1mavmul  18339  mavmulass  18340  marepvcl  18360  1marepvmarrepid  18366  cramerimplem1  18469  hauscmplem  18989  ptbasid  19128  ptpjcn  19164  upxp  19176  uptx  19178  txcmplem2  19195  xkopt  19208  txhmeo  19356  alexsubALTlem3  19601  nrginvrcn  20252  nmoi  20287  nmoleub  20290  cncfmet  20464  cnheibor  20507  evth  20511  pcopt  20574  pcopt2  20575  pcorevlem  20578  pi1xfrf  20605  pi1xfr  20607  pi1xfrcnvlem  20608  iscauf  20771  iscmet3lem1  20782  iscmet3lem2  20783  iscmet3  20784  causs  20789  bcthlem5  20819  bcth3  20822  ovolfcl  20930  ovolfioo  20931  ovolficc  20932  ovolficcss  20933  ovolfsval  20934  ovolmge0  20940  ovollb2lem  20951  ovolunlem1a  20959  ovoliunlem1  20965  ovoliunlem2  20966  ovoliun  20968  ovolicc1  20979  ovolicc2lem3  20982  ovolicc2lem4  20983  ovolicc2lem5  20984  voliunlem1  21011  volsup  21017  ioombl1lem2  21020  ovolfs2  21031  uniioovol  21039  uniiccvol  21040  uniioombllem3a  21044  uniioombllem3  21045  uniioombllem4  21046  uniioombllem5  21047  uniioombllem6  21048  dyadmbl  21060  volcn  21066  ismbf  21088  mbfadd  21119  mbfsub  21120  mbflimsup  21124  0plef  21130  itg1climres  21172  mbfi1fseqlem1  21173  mbfi1fseqlem3  21175  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  mbfmul  21184  xrge0f  21189  itg2ge0  21193  itg2seq  21200  itg2uba  21201  itg2lea  21202  itg2eqa  21203  itg2splitlem  21206  itg2split  21207  itg2i1fseqle  21212  itg2i1fseq  21213  itg2i1fseq2  21214  itg2addlem  21216  bddmulibl  21296  ellimc3  21334  dvaddbr  21392  dvcobr  21400  dvcj  21404  dvfre  21405  dvcnvlem  21428  dvlip  21445  dvlipcn  21446  c1lip1  21449  tdeglem4  21509  tdeglem2  21510  coe1mul3  21551  ply1rem  21615  fta1g  21619  ig1pdvds  21628  plyf  21646  plyeq0lem  21658  plypf1  21660  plyaddlem  21663  plymullem  21664  plyco  21689  dgreq  21692  0dgrb  21694  coefv0  21695  coeaddlem  21696  coemullem  21697  coemulc  21702  plycn  21708  dgrcolem2  21721  plycjlem  21723  plycj  21724  plyrecj  21726  plyreres  21729  dvply1  21730  vieta1lem2  21757  vieta1  21758  elqaalem2  21766  aareccl  21772  aalioulem1  21778  ulmcaulem  21839  ulmcau  21840  ulmcn  21844  mtest  21849  psergf  21857  dvradcnv  21866  psercn2  21868  pserdvlem2  21873  pserdv2  21875  abelthlem6  21881  abelthlem8  21884  abelthlem9  21885  logtayl  22085  amgm  22364  ftalem1  22390  ftalem2  22391  ftalem3  22392  ftalem4  22393  ftalem5  22394  basellem2  22399  muinv  22513  dchrmulcl  22568  dchrinvcl  22572  dchrfi  22574  dchrghm  22575  dchrsum2  22587  dchrsum  22588  bposlem5  22607  lgscllem  22622  lgsval4a  22637  lgsneg  22638  lgsdir  22649  lgsdilem2  22650  lgsdi  22651  lgsne0  22652  lgseisenlem3  22670  rpvmasumlem  22716  dchrmusum2  22723  dchrvmasumiflem1  22730  dchrisum0ff  22736  dchrisum0flblem1  22737  dchrisum0fno1  22740  rpvmasum2  22741  dchrisum0re  22742  dchrisum0lem2a  22746  usgrarnedg  23271  usgraedg4  23273  usgrares1  23291  usgrnloop  23430  cyclispthon  23487  fargshiftf  23490  usgrcyclnl2  23495  4cycl4dv  23521  vdgrnn0pnf  23547  ghgrplem2  23822  lnoadd  24126  lnosub  24127  nmosetre  24132  nmooge0  24135  nmoub3i  24141  nmounbi  24144  phoeqi  24226  ubthlem1  24239  h2hcau  24349  h2hlm  24350  hoscl  25117  homcl  25118  hodcl  25119  hoaddcl  25130  homulcl  25131  homulid2  25172  homco1  25173  homulass  25174  hoadddi  25175  hoadddir  25176  hoeq1  25202  hoeq2  25203  adjsym  25205  nmopsetretALT  25235  nmfnsetre  25249  cnvadj  25264  hhcno  25276  hhcnf  25277  nmopub2tALT  25281  nmopge0  25283  unopf1o  25288  unoplin  25292  counop  25293  nmfnleub2  25298  nmfnge0  25299  hmoplin  25314  eigvalcl  25333  lnop0  25338  hmops  25392  hmopm  25393  nlelchi  25433  leop2  25496  leopadd  25504  leopmuli  25505  leopnmid  25510  hmopidmchi  25523  pjinvari  25563  sticl  25587  fcomptf  25948  rge0scvg  26348  esumcst  26483  esumfzf  26487  esumfsup  26488  esumfsupre  26489  hasheuni  26503  measdivcstOLD  26607  eulerpartlems  26712  eulerpartlemgc  26714  eulerpartlemb  26720  derangsn  27027  subfacp1lem5  27041  subfacp1lem6  27042  pconcon  27089  sconpi1  27097  txsconlem  27098  cvxscon  27101  cvmliftphtlem  27175  cvmlift3lem2  27178  cvmlift3lem4  27180  cvmlift3lem6  27182  ghomgrpilem2  27274  ghomcl  27280  ghomgsg  27281  prodeq2ii  27395  prodmolem2a  27416  iprodcl  27470  faclim  27521  fprb  27553  soseq  27684  heicant  28397  mblfinlem2  28400  itg2addnclem  28414  ftc1anclem1  28438  ftc1anclem2  28439  ftc1anclem4  28441  upixp  28594  fdc  28612  seqpo  28614  incsequz  28615  incsequz2  28616  metf1o  28622  geomcau  28626  sstotbnd2  28644  prdsbnd  28663  ismtyima  28673  ismtyhmeolem  28674  heiborlem3  28683  heiborlem6  28686  heiborlem10  28690  bfplem1  28692  ghomco  28719  mzpclall  29034  mzprename  29057  rexrabdioph  29103  rmydioph  29334  rmxdioph  29336  expdiophlem2  29342  expdioph  29343  pw2f1ocnv  29357  kelac1  29387  rngunsnply  29501  ofsubid  29569  ofdivrec  29571  ofdivcan4  29572  ofdivdiv2  29573  dvconstbi  29579  refsum2cnlem1  29730  climinf  29750  stoweidlem26  29792  stoweidlem60  29826  stoweid  29829  2f1fvneq  30114  wwlktovf  30222  usgra2wlkspthlem2  30268  usgra2pthlem1  30271  el2wlkonotlem  30352  usg2wlkonot  30373  usg2wotspth  30374  frgrancvvdeqlemB  30602  rmsupp0  30750  domnmsuppn0  30751  gsummptnn0fzfv  30777  gsumlsscl  30780  lincfsuppcl  30878  linccl  30879  lincdifsn  30889  lincsum  30894  lincscm  30895  lincscmcl  30897  lincext1  30919  lindslinindimp2lem1  30923  lindslinindimp2lem4  30926  lindslinindsimp2lem5  30927  snlindsntor  30936  lincresunitlem2  30941  lincresunit3lem1  30944  lincresunit3lem2  30945  lincresunit3  30946  lincreslvec3  30947  isldepslvec2  30950  zlmodzxzldeplem3  30975
  Copyright terms: Public domain W3C validator