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

Theorem ffvelrn 5829
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 5547 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 5828 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 468 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5553 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3343 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 462 . 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 1755   ran crn 4828    Fn wfn 5401   -->wf 5402   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414
This theorem is referenced by:  ffvelrni  5830  ffvelrnda  5831  dffo3  5846  foco2  5851  ffnfv  5856  ffvresb  5861  fcompt  5866  fsn2  5870  fvconst  5884  fcofo  5979  cocan1  5982  isocnv  6008  isocnv3  6010  isores2  6011  isopolem  6023  isosolem  6025  fovrn  6222  off  6323  fnwelem  6676  smofvon2  6803  smorndom  6815  omsmolem  7080  omsmo  7081  mapsncnv  7247  2dom  7370  xpdom2  7394  domunsncan  7399  xpmapenlem  7466  fiint  7576  ordiso2  7717  infdifsn  7850  cantnflem1  7885  cantnflem1OLD  7908  wemapwe  7916  wemapweOLD  7917  cnfcom3lem  7924  cnfcom3lemOLD  7932  fseqenlem1  8182  finacn  8208  ackbij1lem12  8388  cofsmo  8426  cfsmolem  8427  cfcoflem  8429  coftr  8430  isf32lem6  8515  isf32lem7  8516  isf34lem7  8536  isf34lem6  8537  acncc  8597  axdc2lem  8605  axdc3lem2  8608  axdc3lem4  8610  axdc4lem  8612  axcclem  8614  ttukeylem6  8671  alephreg  8734  pwcfsdom  8735  canthp1lem2  8807  canthp1  8808  pwfseqlem1  8812  pwfseqlem4a  8815  gruf  8965  fsequb2  11781  axdc4uzlem  11787  seqf1o  11830  hashf1lem1  12191  eqs1  12283  shftf  12551  limsupgre  12942  rlimuni  13011  lo1resb  13025  o1resb  13027  o1of2  13073  o1rlimmul  13079  isercolllem1  13125  isercolllem2  13126  isercolllem3  13127  isercoll  13128  climsup  13130  iseralt  13145  sumeq2ii  13153  summolem2a  13175  isumcl  13211  isumshft  13284  climcndslem2  13295  climcnds  13296  mertenslem2  13327  rpnnen2lem10  13488  ruclem8  13501  ruclem12  13505  3dvds  13578  smueqlem  13668  nn0seqcvgd  13727  algrf  13730  eucalg  13744  phimullem  13836  pcmpt  13936  pcprod  13939  vdwlem11  14034  vdwnnlem3  14040  ramlb  14062  0ram  14063  ramcl  14072  imasaddfnlem  14448  imasaddflem  14450  mhmpropd  15452  ghmsub  15734  cntzmhm  15835  f1omvdconj  15931  pj1ghm  16179  gsumzaddlem  16387  gsumzadd  16388  gsumzaddlemOLD  16389  gsumzaddOLD  16390  dprdfadd  16483  dprdfaddOLD  16490  dprdf1o  16502  subgdmdprd  16504  gsumdixpOLD  16634  gsumdixp  16635  lspcl  16978  psrbaglesupp  17368  psrbaglesuppOLD  17369  psrbaglefi  17374  psrbaglefiOLD  17375  resspsrmul  17422  evlslem4OLD  17517  evlslem4  17518  fvcoe1  17561  psropprmul  17590  00ply1bas  17592  subrgvr1cl  17613  coe1mul2lem1  17618  coe1tmmul  17627  ply1coe  17642  znunit  17837  frlmsslsp  18064  frlmsslspOLD  18065  frlmup2  18068  lindfmm  18097  islindf4  18108  1mavmul  18200  mavmulass  18201  marepvcl  18221  1marepvmarrepid  18227  cramerimplem1  18330  hauscmplem  18850  ptbasid  18989  ptpjcn  19025  upxp  19037  uptx  19039  txcmplem2  19056  xkopt  19069  txhmeo  19217  alexsubALTlem3  19462  nrginvrcn  20113  nmoi  20148  nmoleub  20151  cncfmet  20325  cnheibor  20368  evth  20372  pcopt  20435  pcopt2  20436  pcorevlem  20439  pi1xfrf  20466  pi1xfr  20468  pi1xfrcnvlem  20469  iscauf  20632  iscmet3lem1  20643  iscmet3lem2  20644  iscmet3  20645  causs  20650  bcthlem5  20680  bcth3  20683  ovolfcl  20791  ovolfioo  20792  ovolficc  20793  ovolficcss  20794  ovolfsval  20795  ovolmge0  20801  ovollb2lem  20812  ovolunlem1a  20820  ovoliunlem1  20826  ovoliunlem2  20827  ovoliun  20829  ovolicc1  20840  ovolicc2lem3  20843  ovolicc2lem4  20844  ovolicc2lem5  20845  voliunlem1  20872  volsup  20878  ioombl1lem2  20881  ovolfs2  20892  uniioovol  20900  uniiccvol  20901  uniioombllem3a  20905  uniioombllem3  20906  uniioombllem4  20907  uniioombllem5  20908  uniioombllem6  20909  dyadmbl  20921  volcn  20927  ismbf  20949  mbfadd  20980  mbfsub  20981  mbflimsup  20985  0plef  20991  itg1climres  21033  mbfi1fseqlem1  21034  mbfi1fseqlem3  21036  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mbfmul  21045  xrge0f  21050  itg2ge0  21054  itg2seq  21061  itg2uba  21062  itg2lea  21063  itg2eqa  21064  itg2splitlem  21067  itg2split  21068  itg2i1fseqle  21073  itg2i1fseq  21074  itg2i1fseq2  21075  itg2addlem  21077  bddmulibl  21157  ellimc3  21195  dvaddbr  21253  dvcobr  21261  dvcj  21265  dvfre  21266  dvcnvlem  21289  dvlip  21306  dvlipcn  21307  c1lip1  21310  evlslem3  21365  evl1val  21378  evl1sca  21380  pf1const  21396  tdeglem4  21413  tdeglem2  21414  coe1mul3  21455  ply1rem  21519  fta1g  21523  ig1pdvds  21532  plyf  21550  plyeq0lem  21562  plypf1  21564  plyaddlem  21567  plymullem  21568  plyco  21593  dgreq  21596  0dgrb  21598  coefv0  21599  coeaddlem  21600  coemullem  21601  coemulc  21606  plycn  21612  dgrcolem2  21625  plycjlem  21627  plycj  21628  plyrecj  21630  plyreres  21633  dvply1  21634  vieta1lem2  21661  vieta1  21662  elqaalem2  21670  aareccl  21676  aalioulem1  21682  ulmcaulem  21743  ulmcau  21744  ulmcn  21748  mtest  21753  psergf  21761  dvradcnv  21770  psercn2  21772  pserdvlem2  21777  pserdv2  21779  abelthlem6  21785  abelthlem8  21788  abelthlem9  21789  logtayl  21989  amgm  22268  ftalem1  22294  ftalem2  22295  ftalem3  22296  ftalem4  22297  ftalem5  22298  basellem2  22303  muinv  22417  dchrmulcl  22472  dchrinvcl  22476  dchrfi  22478  dchrghm  22479  dchrsum2  22491  dchrsum  22492  bposlem5  22511  lgscllem  22526  lgsval4a  22541  lgsneg  22542  lgsdir  22553  lgsdilem2  22554  lgsdi  22555  lgsne0  22556  lgseisenlem3  22574  rpvmasumlem  22620  dchrmusum2  22627  dchrvmasumiflem1  22634  dchrisum0ff  22640  dchrisum0flblem1  22641  dchrisum0fno1  22644  rpvmasum2  22645  dchrisum0re  22646  dchrisum0lem2a  22650  usgrarnedg  23125  usgraedg4  23127  usgrares1  23145  usgrnloop  23284  cyclispthon  23341  fargshiftf  23344  usgrcyclnl2  23349  4cycl4dv  23375  vdgrnn0pnf  23401  ghgrplem2  23676  lnoadd  23980  lnosub  23981  nmosetre  23986  nmooge0  23989  nmoub3i  23995  nmounbi  23998  phoeqi  24080  ubthlem1  24093  h2hcau  24203  h2hlm  24204  hoscl  24971  homcl  24972  hodcl  24973  hoaddcl  24984  homulcl  24985  homulid2  25026  homco1  25027  homulass  25028  hoadddi  25029  hoadddir  25030  hoeq1  25056  hoeq2  25057  adjsym  25059  nmopsetretALT  25089  nmfnsetre  25103  cnvadj  25118  hhcno  25130  hhcnf  25131  nmopub2tALT  25135  nmopge0  25137  unopf1o  25142  unoplin  25146  counop  25147  nmfnleub2  25152  nmfnge0  25153  hmoplin  25168  eigvalcl  25187  lnop0  25192  hmops  25246  hmopm  25247  nlelchi  25287  leop2  25350  leopadd  25358  leopmuli  25359  leopnmid  25364  hmopidmchi  25377  pjinvari  25417  sticl  25441  fcomptf  25803  rge0scvg  26232  esumcst  26367  esumfzf  26371  esumfsup  26372  esumfsupre  26373  hasheuni  26387  measdivcstOLD  26491  eulerpartlems  26590  eulerpartlemgc  26592  eulerpartlemb  26598  derangsn  26905  subfacp1lem5  26919  subfacp1lem6  26920  pconcon  26967  sconpi1  26975  txsconlem  26976  cvxscon  26979  cvmliftphtlem  27053  cvmlift3lem2  27056  cvmlift3lem4  27058  cvmlift3lem6  27060  ghomgrpilem2  27151  ghomcl  27157  ghomgsg  27158  prodeq2ii  27272  prodmolem2a  27293  iprodcl  27347  faclim  27398  fprb  27430  soseq  27561  heicant  28267  mblfinlem2  28270  itg2addnclem  28284  ftc1anclem1  28308  ftc1anclem2  28309  ftc1anclem4  28311  upixp  28464  fdc  28482  seqpo  28484  incsequz  28485  incsequz2  28486  metf1o  28492  geomcau  28496  sstotbnd2  28514  prdsbnd  28533  ismtyima  28543  ismtyhmeolem  28544  heiborlem3  28553  heiborlem6  28556  heiborlem10  28560  bfplem1  28562  ghomco  28589  mzpclall  28905  mzprename  28928  rexrabdioph  28974  rmydioph  29205  rmxdioph  29207  expdiophlem2  29213  expdioph  29214  pw2f1ocnv  29228  kelac1  29258  rngunsnply  29372  ofsubid  29440  ofdivrec  29442  ofdivcan4  29443  ofdivdiv2  29444  dvconstbi  29450  refsum2cnlem1  29601  climinf  29622  stoweidlem26  29664  stoweidlem60  29698  stoweid  29701  2f1fvneq  29986  wwlktovf  30094  usgra2wlkspthlem2  30140  usgra2pthlem1  30143  el2wlkonotlem  30224  usg2wlkonot  30245  usg2wotspth  30246  frgrancvvdeqlemB  30474  rmsupp0  30609  domnmsuppn0  30610  gsumlsscl  30622  lincfsuppcl  30653  linccl  30654  lincdifsn  30664  lincsum  30669  lincscm  30670  lincscmcl  30672  lincext1  30694  lindslinindimp2lem1  30698  lindslinindimp2lem4  30701  lindslinindsimp2lem5  30702  snlindsntor  30711  lincresunitlem2  30716  lincresunit3lem1  30719  lincresunit3lem2  30720  lincresunit3  30721  lincreslvec3  30722  isldepslvec2  30725  zlmodzxzldeplem3  30750
  Copyright terms: Public domain W3C validator